The Module Docstring Linter

This file implements a linter that enforces module docstring hygiene:

1. Missing module docstring: warns when a file has no /-! ... -/ block at all (detected on the first non-moduleDoc command).
2. Duplicate module docstrings: warns when a file has more than one /-! ... -/ block (subsequent blocks should be regular /- ... -/ comments).

opaque linter.style.moduleDocstring : Lean.Option Bool

def ModuleDocstringLinter.moduleDocstringLinter : Lean.Linter

The module docstring linter checks two things:

• A file that has no /-! ... -/ block gets a warning on its first non-moduleDoc command.
• A file that has more than one /-! ... -/ block gets a warning on each extra block.

Equations

• One or more equations did not get rendered due to their size.