feat: support fixed integers and conditions in meta-simp-set #346
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
This is helpful for debugging, when we copy the individual statements to the actual proof, which may not have Ctxt open.
Co-authored-by: Siddharth <[email protected]>
Co-authored-by: Siddharth <[email protected]>
…ean-up and extract general theorems
|
This is work in progress. It seems toSnoc_toMap does not work with nested snocs? @[simp]
theorem toSnoc_toMap {Γ : Ctxt Ty} {t : Ty } {var : Ctxt.Var Γ t} {f : Ty → Ty2} :
@Var.toMap _ (Γ.snoc t) _ _ f var.toSnoc = var.toMap.toSnoc := rfl |
|
Alive Statistics: 54 / 93 (39 failed) |
|
Alive Statistics: 54 / 93 (39 failed) |
|
Alive Statistics: 54 / 93 (39 failed) |
|
Alive Statistics: 54 / 93 (39 failed) |
|
LGTM, I am happy to merge this in, with @alexkeizer 's review on it. |
alexkeizer
reviewed
May 27, 2024
|
Alive Statistics: 54 / 93 (39 failed) |
1 similar comment
|
Alive Statistics: 54 / 93 (39 failed) |
|
From my perspective all comments are adressed. @alexkeizer @bollu, could you take a final look? |
|
Alive Statistics: 54 / 93 (39 failed) |
tobiasgrosser
commented
May 28, 2024
|
Reviewed in person by @bollu |
|
Alive Statistics: 54 / 93 (39 failed) |
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.
ConcreteOrMVar.instantiate_ofNat_eqto simplify instantiation and canonicalize to ofNat.Unfortunately, this seems to lead to a 'motive not type correct' error. To resolve it we use simp! that just unfolds. This should be debugged further: #349.
toSnoc_toMapto work on sequences of snoc