1c1bd8e064
This PR fixes `grind` rejecting dot notation terms, mistaking them for
local hypotheses.
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.
### Minimal reproducer
```lean
theorem Nat.triv (n : Nat) : n = n := rfl
example (n : Nat) : n = n := by
grind [n.triv] -- Previously: "redundant parameter `n.triv`"
```
This also 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
|
||
|---|---|---|
| .. | ||
| bench | ||
| bench-radar | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lake | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||