)]}'
{
  "commit": "12797381fdd0670b89f63ba11d1c2707c333683f",
  "tree": "9538b67074dfd63739a613c7b00cbacd9bfac0a3",
  "parents": [
    "19e1fe55f33a8aadc4243da32828b70a4b4677cc"
  ],
  "author": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Wed Dec 10 03:58:27 2025 +0000"
  },
  "committer": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Wed Dec 10 03:58:27 2025 +0000"
  },
  "message": "fix(grind): handle dot notation on local variables in parameters\n\nWhen a grind parameter like `n.triv` is given, where `n` is a local\nvariable and `triv` is a theorem that takes `n` as an argument (so\n`n.triv` means `Nat.triv n`), grind was incorrectly rejecting it with\n\"redundant parameter\" because it detected that the identifier resolved\nto a local variable via `resolveLocalName`.\n\nThe fix checks if `resolveLocalName` returns field projections (non-empty\nlist), indicating dot notation. In that case, we process the parameter\nas a term expression to let elaboration resolve the dot notation properly,\nrather than trying to resolve it as a global constant name.\n\nFixes the issue where `grind [x.exp_pos]` was rejected even though\n`x.exp_pos` elaborates to `Real.exp_pos x`, a valid theorem application.\n\n🤖 Prepared with Claude Code\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "c502c5d15536c95dff0cc118bb086081a4b667be",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Tactic/Grind/Param.lean",
      "new_id": "ec6c1c6e7dd6fa0a29139a5445bbfb1e70f58434",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Tactic/Grind/Param.lean"
    },
    {
      "type": "modify",
      "old_id": "ce57e409da077aeec6488e25a28e63f48dd6119d",
      "old_mode": 33188,
      "old_path": "tests/lean/run/grind_local_hyps.lean",
      "new_id": "1f95d4f679923b4a9a577870de965fd56f17cac7",
      "new_mode": 33188,
      "new_path": "tests/lean/run/grind_local_hyps.lean"
    }
  ]
}