fix(grind): handle dot notation on local variables in parameters When a grind parameter like `n.triv` is given, where `n` is a local variable and `triv` is a theorem that takes `n` as an argument (so `n.triv` means `Nat.triv n`), grind was incorrectly rejecting it with "redundant parameter" because it detected that the identifier resolved to a local variable via `resolveLocalName`. The fix checks if `resolveLocalName` returns field projections (non-empty list), indicating dot notation. In that case, we process the parameter as a term expression to let elaboration resolve the dot notation properly, rather than trying to resolve it as a global constant name. Fixes the issue where `grind [x.exp_pos]` was rejected even though `x.exp_pos` elaborates to `Real.exp_pos x`, a valid theorem application. 🤖 Prepared with Claude Code
This is the repository for Lean 4.
See Install Lean.
Please read our Contribution Guidelines first.
See Building Lean.