)]}'
{
  "commit": "71568b2cf3e8fe4cdd0c4802ee41b001b5bf64a7",
  "tree": "9da78bd827d56ff9fb699037f6ce6d1e89bd200c",
  "parents": [
    "6eb6a364b12c7a0ca710aa5ac9fa9a38f765c618"
  ],
  "author": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Wed Apr 08 10:58:23 2026 +1000"
  },
  "committer": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Wed Apr 08 10:58:23 2026 +1000"
  },
  "message": "fix: skip implicit_reducible for Prop-valued delta-derived instances\n\nAddress review feedback: skip setting `@[implicit_reducible]` on\nProp-valued instances (theorems), matching the behavior of the\nhandwritten `instance` command in `MutualDef.lean`.\n\nCo-Authored-By: Claude Opus 4.6 (1M context) \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "43bfb57e85aba1d8744650f075ff1373469a5368",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Deriving/Basic.lean",
      "new_id": "e8ddf022df65cb4873e6a0de4945a04b72ee62ac",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Deriving/Basic.lean"
    },
    {
      "type": "modify",
      "old_id": "783436ec170bec408e36fb1e37b05c0987cfe686",
      "old_mode": 33188,
      "old_path": "tests/elab/derivingDelta.lean",
      "new_id": "6678c726f64a6d994e42910cf7b39c8ebecee3b8",
      "new_mode": 33188,
      "new_path": "tests/elab/derivingDelta.lean"
    },
    {
      "type": "modify",
      "old_id": "8da1b0cfcd28fa44c754894426f7c9e4e0cb1370",
      "old_mode": 33188,
      "old_path": "tests/elab/deriving_diamond_defeq.lean",
      "new_id": "cfac19f2f51f22236901d6011b677a81e2f9eecc",
      "new_mode": 33188,
      "new_path": "tests/elab/deriving_diamond_defeq.lean"
    }
  ]
}