)]}'
{
  "commit": "6608aedbd10a59260acf0ca25dfb67782c8d25ad",
  "tree": "584fc5cbd25cba7a01bd378d1f63b37fc17ee588",
  "parents": [
    "d3fdb900b59c0c1f7375180f4e87b5e9dfb29881"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sun Sep 20 18:20:21 2026 +0000"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sun Sep 20 18:20:21 2026 +0000"
  },
  "message": "perf: decide `isProofQuick` for applications whose type is a `motive`\n\nThis PR makes `Meta.isProofQuick` return a definite answer for applications such as `match` auxiliary functions, `casesOn`, `brecOn`, and recursors, whose type is a `motive` variable applied to arguments. Previously these fell through to `isProof`\u0027s slow path, which infers the type and reduces it to a sort.\n\n`isArrowProposition\u0027` already handled the case where the codomain of the function type is a de Bruijn variable, by inspecting the sort of the corresponding binder. It now also handles the case where that variable is applied to arguments, by stripping the same number of arrows from the binder type before inspecting its sort. For example, `f.match_1.{u} : (motive : Nat → Sort u) → ... → motive x` instantiated at `u :\u003d 1` is definitely not a proof, and at `u :\u003d 0` it definitely is.\n\nCo-Authored-By: Claude Fable 5.1 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "0e3d57afdffbb1d4d62bb423b8847afa4216af13",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/InferType.lean",
      "new_id": "6b83633413307a5e1a3a29d7b044ccae32af3df6",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/InferType.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "569b377055ac23f59d9b639d5df863aa00ed366a",
      "new_mode": 33188,
      "new_path": "tests/elab/isProofQuickMotive.lean"
    }
  ]
}