)]}'
{
  "commit": "e379768aacb3bf9164198c5b41089d60a5bce0d1",
  "tree": "7a11704e86857a47c8e4f7e2f4d3a049eb9a0ae9",
  "parents": [
    "b4c4f265aade4524c885aebfc4f558583ae8daee"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sat Mar 21 21:06:11 2026 -0700"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sat Mar 21 21:19:33 2026 -0700"
  },
  "message": "feat: add `register_sym_simp` command and `SymSimpVariant` infrastructure\n\nThis PR adds the `register_sym_simp` command for declaring named `Sym.simp`\nvariants with `pre`/`post` simproc chains and optional config overrides.\n\n- `SymSimpVariant` structure storing `pre`/`post` syntax (elaborated at use\n  time) and `Config` overrides\n- `SimpleScopedEnvExtension` for persistent cross-module variant storage\n- `register_sym_simp` command syntax with `sym_simp_field` category\n- Command elaborator parsing fields and registering variants\n- `getSymSimpVariant?` lookup function\n- `deriving Inhabited` on `Simp.Config` for extension support\n\nCo-Authored-By: Claude Opus 4.6 (1M context) \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "94d46ae934dac32a1bc9ac8a5093b9c286f18225",
      "old_mode": 33188,
      "old_path": "src/Init/Sym/Simp/SimprocDSL.lean",
      "new_id": "a66443aa13a27d11a24ac5b36f80a2db97e01e19",
      "new_mode": 33188,
      "new_path": "src/Init/Sym/Simp/SimprocDSL.lean"
    },
    {
      "type": "modify",
      "old_id": "ad054b8f90bfff30e0e8d1474f6907f2826926e9",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Tactic/Grind.lean",
      "new_id": "cb94b6d3c0d4769ad1a955865b565eace513b75f",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Tactic/Grind.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "b340afceac359af79b94af0c6147c7ca79adb213",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Tactic/Grind/RegisterSymSimp.lean"
    },
    {
      "type": "modify",
      "old_id": "6a8ced4dcea436530151d3fa4a69798b690c0d15",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Sym/Simp.lean",
      "new_id": "8d688f104378c11745a95a88bb04473403d4d8f9",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Sym/Simp.lean"
    },
    {
      "type": "modify",
      "old_id": "0034f602eb684a2ecce91d8b618942d6c96b04ec",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Sym/Simp/RegisterCommand.lean",
      "new_id": "de5241999ff2769b20e1160a9ad876226b0766f5",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Sym/Simp/RegisterCommand.lean"
    },
    {
      "type": "modify",
      "old_id": "179e0ddce978a14bece16b98c954065a9012eb30",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Sym/Simp/SimpM.lean",
      "new_id": "974611d943dc2bdbe501b851c5245433ed3f27b8",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Sym/Simp/SimpM.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "9774e770e394c4eea3b9d19ca2af6841bf4402a7",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Sym/Simp/Variant.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "46050e0936fc4e77301994c2c6a5e8db6bfbd494",
      "new_mode": 33188,
      "new_path": "tests/elab/sym_register_variant1.lean"
    }
  ]
}