)]}'
{
  "commit": "60443878e0d66257c3a3a3f3f08871d6ccaa9ea2",
  "tree": "5a3d7e435ce35babaa1209fdc6bb773fa796cd2e",
  "parents": [
    "a2262c40df2b7dfecb8d008cfbe017dffea363de"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sat Oct 24 22:23:16 2026 +0000"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Mon Oct 26 01:56:55 2026 +0000"
  },
  "message": "perf: do not instantiate constant types in `isPropQuick`, `isProofQuick` and `isTypeQuick`\n\nFor a constant head, these predicates instantiated the universe parameters of the constant\u0027s whole type, usually with fresh level metavariables, so the instantiation cache rarely hit; `isDefEqProofIrrel` calls `isProofQuick` on every `isDefEq` problem. They only inspect the binder structure of that type, the levels of the `Sort`s they reach and the levels of constants they recurse into. They now walk the uninstantiated type and substitute just those levels (`LevelSubst`), with `Level.instantiateParams`, which is what `Expr.instantiateLevelParams` applies to each level. Level instantiation does not change the structure of an expression, so the results are the same; the types of free variables and metavariables are not substituted, as before. A differential check against the previous implementation over every 7th constant of `import Lean`, 8 level patterns (including the constant\u0027s own parameter names, swapped, and assigned and unassigned level metavariables) and arities 0 to 8 found no disagreement in 4.4 M calls.\n\nCo-Authored-By: Claude Opus 5.5 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "6b83633413307a5e1a3a29d7b044ccae32af3df6",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/InferType.lean",
      "new_id": "0d06228576675f2cdcead38906751d73f2c712b0",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/InferType.lean"
    }
  ]
}