)]}'
{
  "commit": "56eae2e81a86e66a3ff00c48cbae31dede58f4e4",
  "tree": "1da1fbbdf8ffe7b4aaa830ed6b6e60d66599ce83",
  "parents": [
    "4bf7fa7447eea00cecba8327bb9c9e5f4485f0a7"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sun Mar 22 07:55:47 2026 -0700"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sun Mar 22 08:42:20 2026 -0700"
  },
  "message": "feat: add interactive `simp` tactic for `sym \u003d\u003e` mode\n\nThis PR adds the `simp` tactic to the `sym \u003d\u003e` interactive mode, completing\nthe `Sym.simp` interactive infrastructure.\n\nThe `simp` tactic supports:\n- `simp` — default (identity) variant\n- `simp myVariant` — named variant registered via `register_sym_simp`\n- `simp [thm₁, thm₂]` — default variant with extra rewrite theorems\n- `simp myVariant [thm₁, thm₂]` — named variant with extra theorems\n\nExtra theorems are composed into the variant\u0027s `post` chain via `\u003e\u003e`.\n\nPer-variant persistent caching: each unique (variant name, extra theorem list)\ncombination gets its own `Sym.Simp.State` cache, shared across invocations\nwithin a `sym \u003d\u003e` block. This avoids redundant simplification of identical\nsubterms when `simp` is called repeatedly (e.g., in branching proofs).\n\nCo-Authored-By: Claude Opus 4.6 (1M context) \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "e51d9f9ab9b1d0e130eefe024a7db2313d0a146f",
      "old_mode": 33188,
      "old_path": "src/Init/Grind/Interactive.lean",
      "new_id": "77bb6e67e11abf7a8af8a7ac25a5980c9694a1f0",
      "new_mode": 33188,
      "new_path": "src/Init/Grind/Interactive.lean"
    },
    {
      "type": "modify",
      "old_id": "2a32d76f48a064a9baeb28dc419bf02353c62bfe",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Tactic/Grind/Basic.lean",
      "new_id": "5fe65c1418e2be2e90323ca0bbce1871085cfc62",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Tactic/Grind/Basic.lean"
    },
    {
      "type": "modify",
      "old_id": "cebb22ab90b32e33905ee81299f4a8cb8405b853",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Tactic/Grind/Sym.lean",
      "new_id": "57473898cfd8530204777f80b5204e765d857002",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Tactic/Grind/Sym.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "0e173ebfcb0f692afd4ef99c1c722fed30cd7875",
      "new_mode": 33188,
      "new_path": "tests/elab/sym_simp_interactive1.lean"
    }
  ]
}