1400b95ffb
This PR upstreams the `ToLevel` typeclass from mathlib and uses it to fix the existing `ToExpr` instances so that they are truly universe polymorphic (previously it generated malformed expressions when the universe level was nonzero). We improve on the mathlib definition of `ToLevel` to ensure the class always lives in `Type`, irrespective of the universe parameter. This implements part one of the plan to upstream a derive handler for `ToExpr`, as discussed in #5906 and #5909. --------- Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Tobias Grosser <tobias@grosser.es> |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lean-toolchain | ||