)]}'
{
  "commit": "a0aa17aeaca28cf6955463ace37e1612d6e7944b",
  "tree": "a7c899c2cddea126d68c9fd99f2c48122f3b79f4",
  "parents": [
    "7f0ac8bb3faee199c435405e8b59b5e76bb0ac84"
  ],
  "author": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Sat Jun 13 03:32:04 2026 +0000"
  },
  "committer": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Sat Jun 13 03:32:04 2026 +0000"
  },
  "message": "chore: mark BitVec.flattenList noncomputable\n\nThe structural definition is only a specification; the divide-and-conquer\nflattenListFast (installed via @[csimp]) is the intended runtime implementation.\nMarking flattenList noncomputable removes the slow compiled version entirely, so\nthe csimp\u0027d implementation is guaranteed to be the only one ever used (and\nflattenList drops off the csimpCore audit list of computable @[csimp] targets).\n\nCo-Authored-By: Claude Opus 4.8 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "c96cf9d28ba94365cd57f34e2a7143eebcc14370",
      "old_mode": 33188,
      "old_path": "src/Init/Data/BitVec/Basic.lean",
      "new_id": "1e78d6c6e0b1bf7797225058fd72754316a5d778",
      "new_mode": 33188,
      "new_path": "src/Init/Data/BitVec/Basic.lean"
    },
    {
      "type": "modify",
      "old_id": "c0e1145cb627b68ecc4c53a824b1febe016086ea",
      "old_mode": 33188,
      "old_path": "tests/elab/csimpCore.lean",
      "new_id": "26be0fda7664911dcde009c9b58ae6753be2de4b",
      "new_mode": 33188,
      "new_path": "tests/elab/csimpCore.lean"
    }
  ]
}
