)]}'
{
  "commit": "7b5647652cebb760ae6a3555ff194723891896d1",
  "tree": "94f66b01bd3e25c32cb8e2c4da4efc5c7f18cc20",
  "parents": [
    "c9a3ebfd1989e3174c22c41be60a717419d03d40"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sun Oct 25 06:24:13 2026 +0000"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sun Oct 25 06:24:44 2026 +0000"
  },
  "message": "perf: optimize literal classification and extend numeric literal support\n\nThis PR optimizes literal recognition and improves `grind` support for rational and signed fixed-width integer literals.\n\nReplace value-extractor calls with direct Boolean checks. Add scientific `Rat` recognition and `Int8`/`Int16`/`Int32`/`Int64` extraction and normalization. Fix interpretation of aliased types and handling of literals in match conditions. Add consistency tests covering wrapping, boundaries, metadata, and metavariables.\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "6e5c003b46cf4d0e19c8f69df5d534211273f1d1",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/LitValues.lean",
      "new_id": "7c78dd77ad97491fd575e40be1a6a8b3b0685667",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/LitValues.lean"
    },
    {
      "type": "modify",
      "old_id": "499c1c910e1cb9d14c367d4912081293656b2045",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Internalize.lean",
      "new_id": "ca67bab725654622f333e8c01e7d906b6ac0c46d",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Internalize.lean"
    },
    {
      "type": "modify",
      "old_id": "2f9cebc1efc721908401eb284b023c9504e47a74",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Intro.lean",
      "new_id": "fa8c783f053df168a18a02cd35a3abb1b4e09488",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Intro.lean"
    },
    {
      "type": "modify",
      "old_id": "322359d60beaed1f73b81acefea0217b9b48a8e7",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Types.lean",
      "new_id": "ebcd84e4b6889060518651541b47fe7f70a8eb05",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Types.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "d4b81890b9684fc539974564c7535cf8017eca66",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_rat_matchcond.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "2c3a3fe5d3a96246bf765b39bb01450e7d4effd5",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_sint_matchcond.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "58dff180f888b2a8d16ceb0381a027d7d475d5e6",
      "new_mode": 33188,
      "new_path": "tests/elab/lit_value_classify.lean"
    }
  ]
}