)]}'
{
  "commit": "ef076e7c84594b40a99e92c6f398aea843edf7f0",
  "tree": "fcee68f6d432cc14977953edce1113bd794bd365",
  "parents": [
    "954fb5a762babaa043d0d2986ffddd370abc254b"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Wed Oct 28 01:17:36 2026 +0000"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Wed Oct 28 01:17:36 2026 +0000"
  },
  "message": "fix: avoid kernel argument comparison in `rfl` proofs of equation lemmas\n\nThis PR fixes equation lemmas of structurally recursive functions whose `rfl` proof made the kernel reduce an expensive term, e.g. `f (n+1) x \u003d f n (x * 1103515245 % 5)` failed with kernel deep recursion, and `cbv`, `rw`, and `simp` using such a lemma failed with it.\n\nWhen both sides of the equation are applications of the function being defined, `tryURefl` now proves it by `Eq.refl` of the left-hand side unfolded once. With `Eq.refl lhs`, the kernel first compares the arguments of the two applications, starting with the last one (`x \u003d?\u003d x * 1103515245 % 5`), a comparison that cannot succeed for a recursive call. The proof is still an `rfl` proof, so the lemma\u0027s defeq attributes are unchanged. The duplicate `Lean.Meta.tryURefl` is removed.\n\nCloses #15987\n\nCo-Authored-By: Claude Opus 5.5 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "501b162885f68d425b2893cf78df46c799152248",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/PreDefinition/EqUnfold.lean",
      "new_id": "04b8fc6446e389539e89a693149731b74f5f4554",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/PreDefinition/EqUnfold.lean"
    },
    {
      "type": "modify",
      "old_id": "d877f5dceeff1aec2d378bb1ae1ba973179ef445",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/PreDefinition/Eqns.lean",
      "new_id": "e0ae2bad9798ade29499c82459e9cd578c8b3b14",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/PreDefinition/Eqns.lean"
    },
    {
      "type": "modify",
      "old_id": "675d677d56430a37fe395b3b12264e4e8ca317b7",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/PreDefinition/EqnsUtils.lean",
      "new_id": "ece853abfe6f5082376fead701dbd955eacdb417",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/PreDefinition/EqnsUtils.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "4d1b44880b3aae0a9bdf342eb8dc812b63789232",
      "new_mode": 33188,
      "new_path": "tests/elab/issue15987.lean"
    }
  ]
}