)]}'
{
  "commit": "c3c477d4bafb717c0068e4fb58e4b1a0e5ec8193",
  "tree": "b2c30a9008fa69d78353fbb181a552af1a9231c2",
  "parents": [
    "8038a8b8904f89ad9542c8eda11379f8f006eab1"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Fri Feb 20 21:16:16 2026 -0800"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Fri Feb 20 21:26:36 2026 -0800"
  },
  "message": "fix: bump transparency in `isDefEqProj` for class projections\n\nWhen a class field is marked `@[reducible]`, `isDefEqDelta` unfolds it\nto `.proj` form. `isDefEqProj` must then compare the struct arguments,\nbut the projection\u0027s parameter is instance-implicit. Without bumping to\n`.instances`, instance definitions (which are `[implicit_reducible]`)\ncannot be unfolded, causing `eq_self` to fail. This mirrors the\ntransparency bump that `isDefEqArgs` applies for instance-implicit\nparameters.\n\nCo-Authored-By: Claude Opus 4.6 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "3343566186bc0935990f859e60de63db32a88d29",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/ExprDefEq.lean",
      "new_id": "1541a7964ae81a36371a3c9807615cefcfc26ab4",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/ExprDefEq.lean"
    },
    {
      "type": "modify",
      "old_id": "a91d3985374e2ecfa6465110e7eb86fae89d9242",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Simp/Main.lean",
      "new_id": "ebc9a2ea4eb8b6fcfba26d40228ba993c18168ba",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Simp/Main.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "868e178562c4f2ee4a05fdbb2d10fee1625ba127",
      "new_mode": 33188,
      "new_path": "tests/lean/run/test_simp_reducible_class.lean"
    }
  ]
}