103ed5b54b
This PR fixes `grind` failing when hypotheses contain metavariables (e.g., after `refine`). The root cause was that `abstractMVars` in `withProtectedMCtx` only abstracted metavariables in the target, not in hypotheses, creating a disconnect in grind's e-graph. The fix removes `abstractMVars` and instead resolves delayed metavariable assignments before exiting `withNewMCtxDepth`. `instantiateMVars` refuses to resolve a delayed assignment when the pending assignment is non-ground (contains unassigned expression metavariables). This function converts such delayed assignments to regular ones using `LocalContext.mkLambda`, allowing `instantiateMVars` to resolve them via beta reduction. The mvar internalization warning is also removed since grind now handles mvars. Closes #12242 Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com> |
||
|---|---|---|
| .. | ||
| bench | ||
| bench-radar | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lake | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| CMakeLists.txt | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||