[Merged by Bors] - feat: #noalign command; align.precheck option#663
Closed
[Merged by Bors] - feat: #noalign command; align.precheck option#663
#noalign command; align.precheck option#663Conversation
5e11592 to
344ab48
Compare
Member
|
👍 on the |
Contributor
|
The precheck is great. bors merge |
bors bot
pushed a commit
that referenced
this pull request
Nov 20, 2022
* The `#noalign` command is like `#align` but it doesn't take a lean 4 name. The semantics are that mathport will delete the theorem which would have been translated at this point, and future references will use `sorry` instead. I am unsure how much we will need this, but it is good for documenting intentional deletions. * The `#align` command now checks that the lean 4 declaration (after stripping `ₓ`) exists. It still requires that the lean 4 name be fully qualified, but it will tell you if you tried to reference something that was in scope. (I don't want it to do name resolution on its own because this will make it harder to compare with the lean 3 version.) You can disable the check using `set_option align.precheck false`. * The `mk_iff` command now does name resolution and attaches proper definition info to the input span. * As expected, the precheck caught a ton of naming bugs in ported files.
|
Pull request successfully merged into master. Build succeeded: |
#noalign command; align.precheck option#noalign command; align.precheck option
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 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.
The
#noaligncommand is like#alignbut it doesn't take a lean 4 name. The semantics are that mathport will delete the theorem which would have been translated at this point, and future references will usesorryinstead. I am unsure how much we will need this, but it is good for documenting intentional deletions.The
#aligncommand now checks that the lean 4 declaration (after strippingₓ) exists. It still requires that the lean 4 name be fully qualified, but it will tell you if you tried to reference something that was in scope. (I don't want it to do name resolution on its own because this will make it harder to compare with the lean 3 version.) You can disable the check usingset_option align.precheck false.The
mk_iffcommand now does name resolution and attaches proper definition info to the input span.As expected, the precheck caught a ton of naming bugs in ported files.