Experiment the addition of sealed/unsealed attributes #19029
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
herbelin
added
kind: feature
coqbot-app
bot
added
the
needs: full CI
github-actions
bot
added
the
needs: rebase
The main changes are: - "opaque" is now part of the Declare.Info.t; - at Qed/Defined time, a check is done to determine if there is an attribute which takes precedence over the Qed/Defined keyword; - for non-interactive declaration, either the default value associated to the kind of the declaration is used, or, in some cases, a specific opacity is decided upfront.
herbelin
force-pushed
the
master+sealed-attribute
branch
from
b5d663f
to
e3c91ca
Compare
coqbot-app
bot
removed
the
needs: rebase
herbelin
force-pushed
the
master+sealed-attribute
branch
from
e3c91ca
to
3e40fa2
Compare
github-actions
bot
added
the
needs: rebase
2 tasks
|
Draft PR, removing the milestone. |
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.
The PR experiments an implementation of the proposition made in CEP #42 of attributes
sealedandunsealedthat allows to indicate the opacity of a definition defined non-interactively, and that provides the current role ofQed/Definedwithout having to break the intuitive matching of keywordsTheorem/QedandDefinition/Defined.The main changes are:
Declare.Info.twhile it was before passed as a standalone argument or stored in the program obligation state -> a better idea would be to have them in theCInfo.tactually, since they can be different for different components of a block of definitionsQed/Definedtime, a check is done to determine if there is an attribute which takes precedence over theQed/Definedkeyword`;At the current time, there is a warning in case of a
sealed/Definedorunsealed/Qedmismatch, as well as when the attribute is defined and there is mismatchTheorem/DefinedorDefinition/Qed. But the warning is deactivated because it is too much work to adapt the stdlib to the warning.