mathlib
94285983
- feat(tactic/rcases): add `rintro (x y : t)` support (#4722)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
5 years ago
feat(tactic/rcases): add `rintro (x y : t)` support (#4722) As requested on Zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/rintros/near/213999254
References
#4925 - Make prime-avoidance branch build
Author
digama0
Parents
877a20e3
Loading