mathlib
99c7d22e - chore(*): fixup docs that don't parse/cause linting errors (#7088)

Commit
4 years ago
chore(*): fixup docs that don't parse/cause linting errors (#7088) A couple docs had errors in the way that they were written, leading to them not displaying properly, or causing linting errors. This aims to make the [style_exceptions.txt](https://github.com/leanprover-community/mathlib/blob/master/scripts/style-exceptions.txt) file smaller, and also make the webdocs display them properly, c.f. [here](https://leanprover-community.github.io/mathlib_docs/topology/metric_space/basic.html).
Author
Parents
Loading