mathlib
1332fe1a
- fix(tactic/rcases): more with_desc fail (#11004)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
4 years ago
fix(tactic/rcases): more with_desc fail (#11004) This causes hovers for definitions using `rcases_patt_parse` to print weird stuff for the parser description.
Author
digama0
Parents
0e8cca36
Loading