Skip to content

feat: refactor irevert implementation#175

Merged
MackieLoeffel merged 22 commits into
leanprover-community:masterfrom
HaleOIC:pr-74
Mar 19, 2026
Merged

feat: refactor irevert implementation#175
MackieLoeffel merged 22 commits into
leanprover-community:masterfrom
HaleOIC:pr-74

Conversation

@HaleOIC
Copy link
Copy Markdown
Contributor

@HaleOIC HaleOIC commented Mar 17, 2026

Description

  • Fixes # 69
  • Add Make related type class and instances
  • Add relative complete tactic for irevert

Copy link
Copy Markdown
Collaborator

@MackieLoeffel MackieLoeffel left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for this PR! I looked over it and added a bunch of comments.

Comment thread src/Iris/Tests/Tactics.lean
Comment thread tactics.md
Comment thread src/Iris/ProofMode/Tactics/Revert.lean Outdated
Comment thread src/Iris/ProofMode/Tactics/Revert.lean Outdated
Comment thread src/Iris/ProofMode/Tactics/Revert.lean Outdated
Comment thread src/Iris/Tests/Tactics.lean
Comment thread src/Iris/ProofMode/Tactics/Revert.lean Outdated
Comment thread src/Iris/ProofMode/Tactics/Revert.lean Outdated
Comment thread src/Iris/ProofMode/Tactics/Revert.lean Outdated
Comment thread src/Iris/ProofMode/ClassesMake.lean
Comment thread PORTING.md Outdated
Comment thread src/Iris/Tests/Tactics.lean Outdated
Comment thread src/Iris/ProofMode/Tactics/Revert.lean Outdated
Comment thread src/Iris/ProofMode/Tactics/Revert.lean Outdated
Comment thread src/Iris/ProofMode/Tactics/Revert.lean Outdated
Comment thread src/Iris/ProofMode/Tactics/Revert.lean Outdated
Comment thread src/Iris/ProofMode/Tactics/Revert.lean Outdated
Comment thread src/Iris/ProofMode/Tactics/Revert.lean Outdated
Comment thread src/Iris/ProofMode/Tactics/Revert.lean Outdated
Comment thread src/Iris/ProofMode/Tactics/Revert.lean Outdated
@MackieLoeffel MackieLoeffel mentioned this pull request Mar 18, 2026
3 tasks
@MackieLoeffel
Copy link
Copy Markdown
Collaborator

@HaleOIC Can you rebase this branch on the current master branch (in particular, adapting to #164 )? Then I think it is ready to merge.

@MackieLoeffel MackieLoeffel merged commit f843941 into leanprover-community:master Mar 19, 2026
1 check passed
@MackieLoeffel MackieLoeffel mentioned this pull request Mar 19, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants