)]}'
{
  "commit": "f055dae3ec6b65a2213ca72f5b8e890fc7a172c5",
  "tree": "ec30efb659654dcf4465f941af493c88be3bbe76",
  "parents": [
    "9a3678935dcabf49e2178721279a6f9a1fe2b664"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sun Mar 22 12:08:33 2026 -0700"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sun Mar 22 12:25:42 2026 -0700"
  },
  "message": "feat: adapt non-equality theorems in `mkTheoremFromDecl`\n\n`mkTheoremFromDecl` and `mkTheoremFromExpr` now handle theorems whose\nconclusion is not an equality:\n- `¬ p` → adapted to `p \u003d False` via `eq_false`\n- `p ↔ q` → adapted to `p \u003d q` via `propext`\n- `p` (proposition) → adapted to `p \u003d True` via `eq_true`\n\nThis enables `Sym.simp` to use hypotheses like `h : p x` as rewrite\nrules that replace `p x` with `True`.\n\nCo-Authored-By: Claude Opus 4.6 (1M context) \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "c888e3cd050b0f6e6d53a248fe218736728e9efa",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Sym/Simp/Theorems.lean",
      "new_id": "c31e404ba24523c15bcb093f880056854f344455",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Sym/Simp/Theorems.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "14774ffbdbdd56e86c3388e76af642c43c60379b",
      "new_mode": 33188,
      "new_path": "tests/elab/sym_simp_adapt1.lean"
    }
  ]
}