)]}'
{
  "commit": "5106517bbea6308402aad73528d396c2777bd51e",
  "tree": "2c375f74dbd26b5f041ee8f13c9823e2509fca2a",
  "parents": [
    "a08dc72dd43698ba5488a00ab03831d11a749c38"
  ],
  "author": {
    "name": "Kim Morrison",
    "email": "qim.morrison@gmail.com",
    "time": "Wed Jul 01 09:20:49 2026 +1000"
  },
  "committer": {
    "name": "Kim Morrison",
    "email": "qim.morrison@gmail.com",
    "time": "Wed Jul 01 09:20:49 2026 +1000"
  },
  "message": "fix: expose `Array.back`, `back!`, and `back?`\n\nThis PR marks `Array.back`, `Array.back!`, and `Array.back?` as `@[expose]`, so that in a downstream module their bodies are available for definitional reduction. Previously `decide` (and even `decide +kernel`) could not evaluate goals such as `#[1, 2, 3].back? \u003d some 3` from another module, even though the `getElem?`/`size` accessors these functions are defined in terms of, and the neighbouring `Array.singleton`, are already exposed.\n\nCo-Authored-By: Claude Opus 4.8 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "3104770cdfad0607acef5d674b5147776c1f41b2",
      "old_mode": 33188,
      "old_path": "src/Init/Data/Array/Basic.lean",
      "new_id": "b38a6238cdc84ebe5349e1fe1753dbc94310a295",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Array/Basic.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "6543247bbf429b06a288f1521e581c0b5e14851a",
      "new_mode": 33188,
      "new_path": "tests/elab/exposeArrayBack.lean"
    }
  ]
}