feat: allow structure in mutual blocks
#6125
Merged
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
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Nov 19, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Nov 19, 2024
leanprover-community-bot
added
the
breaks-mathlib
|
Mathlib CI status (docs):
|
kmill
added a commit
to kmill/lean4
that referenced
this pull request
Nov 22, 2024
…es/structures This PR is a prerequisite for leanprover#6125.
mutual inductive framework later: deal with staging for attribute structure parents: no autobound implicits mutual structure worked, default values buggy mutual defaults passed test suite combine cases add test more sophisticated metavariable solving in checkResultingUniverses refinements to universe inference, better errors recover structure-field-specific universe error messages cleanup refinements, another improvement to collectUniverses error
kmill
force-pushed
the
mutual_structs2
branch
from
b910fdf
to
aefcb51
Compare
kmill
added a commit
to kmill/lean4
that referenced
this pull request
Nov 22, 2024
Closes leanprover#6140. This was fixed by leanprover#6125.
kmill
added a commit
to kmill/lean4
that referenced
this pull request
Nov 22, 2024
…`inductive`s Making use of leanprover#6125.
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 adds support for
structureinmutualblocks, allowing inductive types defined byinductiveandstructureto be mutually recursive. The limitations are (1) that the parents in theextendsclause must be defined before themutualblock and (2) mutually recursive classes are not allowed (a limitation shared byclass inductive). There are also improvements to universe level inference for inductive types and structures. Breaking change: structure parents now elaborate with the structure in scope (fix: use qualified names or rename the structure to avoid shadowing), and structure parents no longer elaborate with autoimplicits enabled.Internally, this is a large refactor of both the
inductiveandstructurecommands. Common material is now inLean.Elab.MutualInductive, and each command plugs into this mutual inductive elaboration framework with the logic specific to the respective command. For example,structurehas code to add projections after the inductive types are added to the environment.Closes #4182