feat: upstream ToLevel from mathlib
#6285
Open
+64
−18
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
|
awaiting-review |
kmill
reviewed
Dec 2, 2024
| prelude | ||
| import Lean.Expr | ||
|
|
||
| /-! # `ToLevel` class |
There was a problem hiding this comment.
Suggested change
| /-! # `ToLevel` class | |
| /-! | |
| # `ToLevel` class |
Comment on lines
+22
to
+24
| /-- The universe itself. This is only here to avoid the "unused universe parameter" error. | ||
| We'll remove this field once https://github.com/leanprover/lean4/issues/2116 gets fixed. | ||
| -/ |
There was a problem hiding this comment.
Some tweaks to emphasize that it's a hack and to deemphasize any promises that it'll ever be removed (I hope it does, but I haven't heard any motion on 2116 one way or another yet)
Suggested change
| /-- The universe itself. This is only here to avoid the "unused universe parameter" error. | |
| We'll remove this field once https://github.com/leanprover/lean4/issues/2116 gets fixed. | |
| -/ | |
| /-- A hack to avoid the "unused universe parameter" error. | |
| We can remove this field pending issue https://github.com/leanprover/lean4/issues/2116 -/ |
| /-- The universe itself. This is only here to avoid the "unused universe parameter" error. | ||
| We'll remove this field once https://github.com/leanprover/lean4/issues/2116 gets fixed. | ||
| -/ | ||
| univ : ∃ x, x = PUnit.unit.{u} := ⟨_, rfl⟩ |
There was a problem hiding this comment.
It really doesn't matter, but some alternative encodings if you want:
Suggested change
| univ : ∃ x, x = PUnit.unit.{u} := ⟨_, rfl⟩ | |
| univ : PUnit.{u} → True := fun _ => trivial |
Suggested change
| univ : ∃ x, x = PUnit.unit.{u} := ⟨_, rfl⟩ | |
| univ : ∀ x : PUnit.{u}, x = x := fun _ => rfl |
Or, for fun, one that doesn't make use of anything but the basic logic:
Suggested change
| univ : ∃ x, x = PUnit.unit.{u} := ⟨_, rfl⟩ | |
| univ : ∀ (_ : Sort u) (p : Prop), p → p := fun _ _ h => h |
|
|
||
| namespace Lean | ||
|
|
||
| universe w |
There was a problem hiding this comment.
Given that Lean core makes use of autoImplicit, could you remove this universe command and the universe u v command later on?
| | none => mkApp (mkConst ``Option.none [levelZero]) type | ||
| | some a => mkApp2 (mkConst ``Option.some [levelZero]) type (toExpr a), | ||
| toTypeExpr := mkApp (mkConst ``Option [levelZero]) type } | ||
| | none => mkApp (mkConst ``Option.none [l.toLevel]) type |
There was a problem hiding this comment.
I think the style should be using toLevel.{u} rather than naming the ToLevel instance:
Suggested change
| | none => mkApp (mkConst ``Option.none [l.toLevel]) type | |
| | none => mkApp (mkConst ``Option.none [toLevel.{u}]) type |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR upstreams the
ToLeveltypeclass from mathlib and uses it to fix the existingToExprinstances so that they are truly universe polymorphic (previously it generated malformed expressions when the universe level was nonzero). We improve on the mathlib definition ofToLevelto ensure the class always lives inType, 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.