mathlib3
e74e5349
- doc(tactic/wlog): use markdown lists rather than indentation (#15113)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
doc(tactic/wlog): use markdown lists rather than indentation (#15113) The indentation used in this docstring was lost in the web docs.
Author
eric-wieser
Parents
0bc51f02
Loading