)]}'
{
  "commit": "2579c8542feaba0e23a3c57aac6bcb66752368af",
  "tree": "139c88c85b0559c34dd6e11b1cac760447533704",
  "parents": [
    "c9708e7bd7cf47106e2fc063d3c586c8f333e54d"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sun Mar 22 10:28:43 2026 -0700"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sun Mar 22 10:32:37 2026 -0700"
  },
  "message": "feat: add sanity checks to `register_sym_simp`\n\nThis PR adds validation to the `register_sym_simp` command:\n- reject duplicate variant names\n- validate `pre`/`post` syntax by elaborating them via `elabSymSimproc`\n  in a minimal `GrindTacticM` context, catching unknown theorem names\n  and unknown theorem set references at registration time\n\nCo-Authored-By: Claude Opus 4.6 (1M context) \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "b340afceac359af79b94af0c6147c7ca79adb213",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Tactic/Grind/RegisterSymSimp.lean",
      "new_id": "63d89839a5741fb8ef9dd001b47ff5caf4a7461d",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Tactic/Grind/RegisterSymSimp.lean"
    },
    {
      "type": "modify",
      "old_id": "0e173ebfcb0f692afd4ef99c1c722fed30cd7875",
      "old_mode": 33188,
      "old_path": "tests/elab/sym_simp_interactive1.lean",
      "new_id": "933a7b874919cb3ad0fc33cee856c23be0c759bb",
      "new_mode": 33188,
      "new_path": "tests/elab/sym_simp_interactive1.lean"
    }
  ]
}