a972c4f50d
This PR fixes a bug where `grind?` suggestions would not include parameters using local variable dot notation (e.g., `cs.getD_rightInvSeq` where `cs` is a local variable). These parameters were incorrectly filtered out because the code assumed all ident params resolve to global declarations. In fact, local variable dot notation produces anchors that need the original term to be loaded during replay, so they must be preserved in the suggestion. Closes #12185 🤖 Prepared with Claude Code Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com> |
||
|---|---|---|
| .. | ||
| bench | ||
| bench-radar | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lake | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||