)]}'
{
  "commit": "96620bed69d36b4bd7382b5b8463ff78fa960194",
  "tree": "e63e0d8d3bf866d460c2e69e594ceb529944b7b3",
  "parents": [
    "b9c9eb9a3acefaa242c1da2a31e3723e94fde3a5"
  ],
  "author": {
    "name": "Sebastian Ullrich",
    "email": "sebasti@nullri.ch",
    "time": "Thu Aug 27 09:44:25 2026 +0000"
  },
  "committer": {
    "name": "Sebastian Ullrich",
    "email": "sebasti@nullri.ch",
    "time": "Thu Aug 27 13:19:32 2026 +0000"
  },
  "message": "feat: allow `optParam` and `autoParam` in implicit binders\n\nThis PR allows default values and auto-param tactics on implicit binders, as in `{n : Nat :\u003d 5}` and `{h : i \u003c n :\u003d by omega}`. Such a parameter is solved by unification like a regular implicit argument; the default value or tactic is used only if unification leaves it unassigned.\n\nPreviously this syntax was a parse error, and an `optParam`/`autoParam` annotation reaching an implicit binder by other means was silently ignored.\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "b72a9e10f27f1a68631935a63623f43ea5fdc36a",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/App.lean",
      "new_id": "67ba0c89428eefbdf074c11c503997d1e79f96a7",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/App.lean"
    },
    {
      "type": "modify",
      "old_id": "11f38a712a1b2233d5a315c2f28f444b04e00086",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Binders.lean",
      "new_id": "1b5a4180f8d2a35cb3c298976f3d160ab438d199",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Binders.lean"
    },
    {
      "type": "modify",
      "old_id": "a99631315f574c3b131e51590af06dc157cf3431",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/BuiltinCommand.lean",
      "new_id": "d27d3b81bdc5310f02cf350053e496509b4e2e98",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/BuiltinCommand.lean"
    },
    {
      "type": "modify",
      "old_id": "998561d235aaa5ba79515d7fff4b19685578399c",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Command.lean",
      "new_id": "77f125fd9a81072637a943779c009738ce4b8d50",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Command.lean"
    },
    {
      "type": "modify",
      "old_id": "27fb5dac6b1e1cd562464c6a076630b4dc63ff91",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/ConfigEval/Builtins.lean",
      "new_id": "444ba5bad8de58c8c6041c42c5ba058aa04e128d",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/ConfigEval/Builtins.lean"
    },
    {
      "type": "modify",
      "old_id": "7b7f039bfa57aef97a3e44348d0f6194fa95fda9",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/SyntheticMVars.lean",
      "new_id": "cfffdbdca1ff253c591efcfd8940ad72db29862a",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/SyntheticMVars.lean"
    },
    {
      "type": "modify",
      "old_id": "7ed8b5b6f3c75b4cdf0a72418927653923bdad2c",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Term/TermElabM.lean",
      "new_id": "587549631b63800f49bada8fe1582c32bcd91ff5",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Term/TermElabM.lean"
    },
    {
      "type": "modify",
      "old_id": "f08650b1760f1dceff189043691cd5b4162b0445",
      "old_mode": 33188,
      "old_path": "src/Lean/Parser/Term/Basic.lean",
      "new_id": "a88f51ef1671e13e29fcdd974c88b97b1c34b9c0",
      "new_mode": 33188,
      "new_path": "src/Lean/Parser/Term/Basic.lean"
    },
    {
      "type": "modify",
      "old_id": "b0a25944216f1812aa0ff7d4d4685bb89f89dde9",
      "old_mode": 33188,
      "old_path": "src/Lean/PrettyPrinter/Delaborator/Builtins.lean",
      "new_id": "669b01756b7314833f848d73108fec8eed732d95",
      "new_mode": 33188,
      "new_path": "src/Lean/PrettyPrinter/Delaborator/Builtins.lean"
    },
    {
      "type": "modify",
      "old_id": "04d7f70f4cbf5a6ee7ee8752f2ac5ca7493659cf",
      "old_mode": 33188,
      "old_path": "src/lake/Lake/Util/Binder.lean",
      "new_id": "79f2e78206819a0fdcff797407ece0fcd6f5485f",
      "new_mode": 33188,
      "new_path": "src/lake/Lake/Util/Binder.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "bf1c51a8acaa33f32cfebd5c69d28f669212b25d",
      "new_mode": 33188,
      "new_path": "tests/elab/implicitAutoParam.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "7f36cc6bbe5ada4333b2cd401b8227cc890bb36c",
      "new_mode": 33188,
      "new_path": "tests/elab/implicitAutoParamClass.lean"
    }
  ]
}