feat: implement imodintro and imod - #141
Merged
Merged
Conversation
MackieLoeffel
force-pushed
the
msammler/imodintro
branch
from
January 30, 2026 09:26
f16bd82 to
bb5bf3c
Compare
MackieLoeffel
force-pushed
the
msammler/imodintro
branch
from
January 30, 2026 10:28
bb5bf3c to
e06618f
Compare
MackieLoeffel
changed the title
MackieLoeffel
force-pushed
the
msammler/imodintro
branch
from
January 30, 2026 13:45
24290a1 to
16cf40a
Compare
MackieLoeffel
force-pushed
the
msammler/imodintro
branch
from
January 30, 2026 13:49
16cf40a to
40aeb09
Compare
Collaborator
Author
|
@lzy0505 This PR is ready to review. |
Collaborator
|
Great PR! I’ve added some code comments. A minor improvement would be the error message for |
lzy0505
approved these changes
Feb 1, 2026
Collaborator
Author
|
Thanks for the review and the changes! It is a bit tricky to tweak the error for |
lzy0505
added a commit
to lzy0505/iris-lean
that referenced
this pull request
Mar 2, 2026
* feat: implement imodintro * feat: add instances for Later and Plainly * feat: add imod --------- Co-authored-by: Zongyuan Liu <liuzongyuan0505@gmail.com>
This was referenced Apr 7, 2026
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
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.
Description
This PR implements the
imodintrotactic and adds the!>intro pattern for introducing modalities.Additionally, it implements
imodand the>cases pattern.Checklist
PORTING.mdas appropriateauthorssection of any appropriate files