feat: finish annotating porting status of proofmode#379
Open
MackieLoeffel wants to merge 2 commits intomasterfrom
Open
feat: finish annotating porting status of proofmode#379MackieLoeffel wants to merge 2 commits intomasterfrom
MackieLoeffel wants to merge 2 commits intomasterfrom
Conversation
Implement the iframe tactic and make it available in specialization patterns and cases patterns. Additional implement input / output handling to IPM synthesis roughly in the style of Hint Mode in Rocq. See the comment on `ParamKind` for a detailed description: The parameters of a class declared with `ipm_class` are categorized into the following categories: 1. in: This is the default for a parameter when not annotated in another way. 2. out: These are parameters marked with `outParam`. These parameters must be mvars when starting typeclass search. 3. semiOut: These are parameters marked with `semiOutParam`. The preceding parameter must be of type `InOut`. The value of the `InOut` parameter decides whether the `semiOut` parameter is treated as an input or an output. 4. uncheckedIn: These are parameters marked with `uncheckedInParam`. These behave like `in` parameters, but allow mvars to match terms (see below). 5. inout: Parameters of type `InOut`, must appear before semiOut parameters (see above). The following constraints apply to the parameters: (In the following, semiOut parameters are treated as inputs if the preceding `InOut` is `in` and as outputs if the `InOut` is `out`.) 1. semiOut parameters must have a preceding `InOut` parameter. 2. For each synthesis problem, all output parameters must be mvars. 3. When an input parameter is a mvar, it is not considered to match an instance which does not have an mvar at the top-level. This is to prevent accidentally instantiating mvars. Note that this only applies for mvars the top-level (matching the behavior of Hint Mode : ! in Rocq), since this is the simplest version to implement and catches most (all?) of the cases.
- Complete pass over the proofmode files to add the rocq_alias annotations - Add rocq_concept annotations for the tactics - Remove the proofmode section in PORTING.md, it is replaced by the status website
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
1 participant
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.
Description
Based on #378 to not create conflicts on the porting annotations