Move to 2025 format version 2.0.0 #6
Merged
Conversation
This file contains hidden or 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
Adds `isReflexive` to inductive data Uses `numNested` instead of `isNested` Ensure all uparams instead of relying on appearance in type Ensure all of an inductive's constructors are dumped Removes the Init.export example for size (Init has grown over time)
The ability to ask for unsafe declarations to be exported is useful for creating test data or counter-examples. It's much easier and less error-prone to write these in Lean as unsafe declarations and export them as such than it is to try and write them from primitives in an external tool.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
Implements the format changes described here
Adds an option to export unsafe declarations, to be used for creating test cases/counter examples
Ensures mdata nodes are removed from expressions
Ensures all uparams are exported, even if they don't show up in the declaration's type (needed for some new Mathlib declarations, esp in CategoryTheory there's occasionally a floating
tuparam).Ensures all constructors are exported even if unused (this is necessary for one of the BoundedChannel declarations)
Updates the examples (removes Init for size)
Bump semver
In the interest of disclosure, the README currently links to Type Checking in Lean 4 since the format is fully documented there. I don't mind if that documentation is copied elsewhere or if the link is redirected somewhere more appropriate, I just did it out of convenience.