New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore: bump std4 dependency #9426
Conversation
@@ -4,7 +4,7 @@ | |||
[{"url": "https://github.com/leanprover/std4", | |||
"type": "git", | |||
"subDir": null, | |||
"rev": "d8610e1bcb91c013c3d868821c0ef28bf693be07", |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
For reference: leanprover-community/batteries@d8610e1...0f6bc5b
/-- For every hypothesis `h : a ~ b` where a `@[symm]` lemma is available, | ||
add a hypothesis `h_symm : b ~ a`. -/ | ||
elab "symm_saturate" : tactic => liftMetaTactic1 fun g => g.symmSaturate | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Has this been moved to Std, or just deleted? The Std commit log doesn't make any such move obvious.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is only used by solve_by_elim
, and moved to Std as part of leanprover-community/batteries#447
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah sorry, I was foiled by "load diff" banners blocking my ability to Ctrl+F!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
bors d+
Thanks!
✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
This is quite a substantial bump as `Nondet` / `backtrack` / `solve_by_elim` have all moved to Std. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Pull request successfully merged into master. Build succeeded: |
This is quite a substantial bump as
Nondet
/backtrack
/solve_by_elim
have all moved to Std.Infelicities:
Except.emoji
has becomeprivate
in Std, so for now I've just made several copies of it here, at each point of use. feat: make Except.emoji public batteries#506 makes it public again.MVarId.note
is now inStd.Tactic.SolveByElim
, so we need to (otherwise unnecessarily) import that. chore: move MVarId.note batteries#507 fixes this.