)]}'
{
  "commit": "3a69f8f3f254150ac8fbdaba508978e613deeb0a",
  "tree": "be1c5c1a8fef97c8e2e5439e2d4dae9cbf357034",
  "parents": [
    "b858d0fbf284f9d2ec05429d07554b2deb80bc79"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sun Mar 22 14:25:38 2026 -0700"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sun Mar 22 14:41:25 2026 -0700"
  },
  "message": "feat: support local hypotheses in `simp [h]` for `sym \u003d\u003e` mode\n\nThe `simp` tactic in `sym \u003d\u003e` mode now resolves identifiers in the extra\ntheorem list against local hypotheses first, falling back to global\nconstants. Local hypotheses are adapted via `mkTheoremFromExpr` (using\nthe `eq_true`/`eq_false`/`propext` adapter from #13041).\n\n- Add `ExtraTheorem` inductive (`.const` / `.fvar`) for cache keying\n- Add `resolveExtraTheorem` that checks the local context before globals\n- Update `addExtraTheorems`, `mkDefaultMethods`, `elabVariant` signatures\n\nCo-Authored-By: Claude Opus 4.6 (1M context) \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "5fe65c1418e2be2e90323ca0bbce1871085cfc62",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Tactic/Grind/Basic.lean",
      "new_id": "228ff2bfa68af17189054af1d6ad7cffc2f8921b",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Tactic/Grind/Basic.lean"
    },
    {
      "type": "modify",
      "old_id": "57473898cfd8530204777f80b5204e765d857002",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Tactic/Grind/Sym.lean",
      "new_id": "62c83e8b52ea4fb5011a38889e661511fc5cac95",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Tactic/Grind/Sym.lean"
    },
    {
      "type": "modify",
      "old_id": "14774ffbdbdd56e86c3388e76af642c43c60379b",
      "old_mode": 33188,
      "old_path": "tests/elab/sym_simp_adapt1.lean",
      "new_id": "26af049e2461ebf42b3b3207c9d3f2193b8b236d",
      "new_mode": 33188,
      "new_path": "tests/elab/sym_simp_adapt1.lean"
    }
  ]
}