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] - feat: port split_ifs tactic #508
Conversation
(See #505 for some initial discussion.) |
@dwrensha, I migrated the tests over from mathlib3, and in fact detected a regression by doing so. I've left your branch broken with the failing test in place, so you can find it easily. :-) Feel free to either comment out the test explaining what's going on, or fix it, as seems most appropriate! |
Updated. The tests pass after I map Lean 3 |
bors merge |
This is intended to be as close as possible of a translation of the mathlib3 version: https://github.com/leanprover-community/mathlib/blob/12a7da107a39ef936c5d4a8cb873018ad05b07a6/src/tactic/split_ifs.lean Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Pull request successfully merged into master. Build succeeded: |
This is intended to be as close as possible of a translation of the mathlib3 version: https://github.com/leanprover-community/mathlib/blob/12a7da107a39ef936c5d4a8cb873018ad05b07a6/src/tactic/split_ifs.lean