mathlib3
0ea3dfe4
- feat(tactic/rcases): transport the `cases h : e` syntax to `rcases` (#1611)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
6 years ago
feat(tactic/rcases): transport the `cases h : e` syntax to `rcases` (#1611) * Update rcases.lean * Update rcases.lean * Update rcases.lean * Update lift.lean * Update rcases.lean * Update tactics.md * Update rcases.lean
References
#1611 - feat(tactic/rcases): transport the `cases h : e` syntax to `rcases`
Author
cipher1024
Committer
mergify[bot]
Parents
7a8f53e1
Loading