The Module Docstring Linter #
This file implements a linter that checks that every file has at most one
module docstring (a /-! ... -/ block). If more than one is present, the
extra ones are flagged with a warning suggesting they be converted to regular
multiline comments (/- ... -/).
The module docstring linter warns when a file contains more than one
/-! ... -/ block. The first such block is the module docstring; all
subsequent ones should be regular comments (/- ... -/).
Equations
- One or more equations did not get rendered due to their size.