fix: inductive elaboration should keep track of universe level parameters created in binders
#5814
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
…meters created in binders
Refactors `inductive` elaborator to keep track of universe level parameters created during elaboration of `variable`s and binders. This fixes an issue in Mathlib where their `Type*` elaborator can result in unexpected universe levels.
For example, in
```lean4
variable {F : Type*}
inductive I1 (A B : Type*) (x : F) : Type
```
before this change the signature would be
```
I1.{u_1, u_2} {F : Type u_1} (A : Type u_1) (B : Type u_2) (x : F) : Type
```
but now it is
```
I1.{u_1, u_2, u_3} {F : Type u_1} (A : Type u_2) (B : Type u_3) (x : F) : Type
```
Fixes this for the `axiom` elaborator too.
Adds more accurate universe level validation for mutual inductives.
Breaking change: removes `Lean.Elab.Command.expandDeclId`. Use `Lean.Elab.Term.expandDeclId` from within `runCommandElabM`.
github-actions
bot
added
the
toolchain-available
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Oct 23, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Oct 23, 2024
leanprover-community-bot
added
the
breaks-mathlib
|
Mathlib CI status (docs):
|
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Oct 23, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Oct 23, 2024
leanprover-community-bot
added
builds-mathlib
tobiasgrosser
pushed a commit
to opencompl/lean4
that referenced
this pull request
Oct 27, 2024
…meters created in binders (leanprover#5814) Refactors `inductive` elaborator to keep track of universe level parameters created during elaboration of `variable`s and binders. This fixes an issue in Mathlib where its `Type*` elaborator can result in unexpected universe levels. For example, in ```lean4 variable {F : Type*} inductive I1 (A B : Type*) (x : F) : Type ``` before this change the signature would be ``` I1.{u_1, u_2} {F : Type u_1} (A : Type u_1) (B : Type u_2) (x : F) : Type ``` but now it is ``` I1.{u_1, u_2, u_3} {F : Type u_1} (A : Type u_2) (B : Type u_3) (x : F) : Type ``` Fixes this for the `axiom` elaborator too. Adds more accurate universe level validation for mutual inductives. Breaking change: removes `Lean.Elab.Command.expandDeclId`. Use `Lean.Elab.Term.expandDeclId` from within `runCommandElabM`.
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.
Refactors
inductiveelaborator to keep track of universe level parameters created during elaboration ofvariables and binders. This fixes an issue in Mathlib where itsType*elaborator can result in unexpected universe levels.For example, in
before this change the signature would be
but now it is
Fixes this for the
axiomelaborator too.Adds more accurate universe level validation for mutual inductives.
Breaking change: removes
Lean.Elab.Command.expandDeclId. UseLean.Elab.Term.expandDeclIdfrom withinrunCommandElabM.