42ab5dfab0
This PR makes two improvements to the local context when there are autobound implicits in `variable`s. First, the local context no longer has two copies of every variable (the local context is rebuilt if the types of autobound implicits have metavariables). Second, these metavariables get names using the same algorithm used by binders that appear in declarations (with `mkForallFVars'` instead of `mkForallFVars`). This removes the last use of `Term.addAutoBoundImplicits'`, which inherently has this variable duplication issue. |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lean-toolchain | ||