mathlib
bbd0f769
- chore(*): clean up comment strings in docstrings (#11557)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
4 years ago
chore(*): clean up comment strings in docstrings (#11557) The syntax for these was wrong and showed up in doc-gen output unintentionally e.g. https://leanprover-community.github.io/mathlib_docs/algebra/group/opposite.html#add_monoid_hom.op
Author
alexjbest
Parents
a90f9692
Loading