642bcdf55a
This PR fixes a bug where `grind [foo]` fails when the theorem `foo` has a different universe variable name than the goal, even though universe polymorphism should allow the universes to unify. The issue was in `instantiateGroundTheorem` (used for theorems with no quantified parameters), which was passing `thm.proof` directly instead of calling `getProofWithFreshMVarLevels`. This meant ground theorems retained their original universe level params instead of getting fresh level metavariables that could unify with the goal's universe levels. Fixes https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/grind.20fails.20because.20of.20universe.20variable.20name 🤖 Prepared with Claude Code Co-authored-by: Claude <noreply@anthropic.com> |
||
|---|---|---|
| .. | ||
| bench | ||
| bench-radar | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lake | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| CMakeLists.txt | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||