)]}'
{
  "commit": "24536f4b09996ac7079abd781e59226bcf7c2704",
  "tree": "680a54f85df01e21c64391fb4bcf1bc5d80178ca",
  "parents": [
    "7b9a131805fcd59f59c01e2674647354a0c69709"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Thu Oct 22 04:32:10 2026 +0000"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Thu Oct 22 04:32:10 2026 +0000"
  },
  "message": "fix: interpret literals in `grind` only when their type is in normal form\n\nThis PR fixes `grind` producing a proof the kernel rejects (`decide (1 \u003d 1) \u003d false`) when the same literal occurs at definitionally equal but syntactically different types, such as `(1 : BitVec w)` and `(1 : BitVec 32)` for `@[implicit_reducible] def w : Nat :\u003d 32`.\n\n`LitValues` recognizes literals up to `whnfD` on their types, so `(1 : BitVec w)` was an interpreted term with the same value as `(1 : BitVec 32)`. The canonicalizer runs at reducible transparency and does not unfold `w`, so the two remained distinct interpreted nodes in the E-graph. When model-based theory combination proposed equating them, `addEqStep` treated them as distinct values and `closeGoalWithValuesEq` built an invalid proof. With a semireducible `w`, the same path failed earlier with `failed to synthesize Decidable (1 \u003d 1)`.\n\n`isInterpreted` now requires the literal\u0027s type to be, structurally, a literal type with a normal form: `Nat`, `Int`, `String`, `Char`, `UInt8`, `UInt16`, `UInt32`, `UInt64`, or `Fin n`/`BitVec n` where `n` is a numeral. This also subsumes the explicit `Float`/`Float32` exclusion, since those types are not in the list.\n\nCloses #15541\n\nCo-Authored-By: Claude Opus 5.5 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "e35be6b07eb5a83f7df354846e32bff630eb6a0d",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Types.lean",
      "new_id": "5368aca297a5cf2172ce15251776b6693b65b309",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Types.lean"
    },
    {
      "type": "modify",
      "old_id": "ae70415acf119c53d5448376e52d1f6b475b1332",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_15541.lean",
      "new_id": "72c1e453b1d33b69ed07d71c6ac9f403fee04aab",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_15541.lean"
    }
  ]
}