FormalConjecturesTest/Util/Linters/ModuleDocstringLinter.lean

GitHub source file

0 declarations, 0 contain sorry, 0 declared as axioms

Tests for the module docstring linter

This file tests that the module docstring linter:

  1. Does not flag the first /-! ... -/ block.
  2. Flags files with more than one /-! ... -/ block.
  3. Can be disabled with set_option.

The "missing module docstring" warning is tested in ModuleDocstringLinterMissing.lean.

Imports (1)
Imported by 1 file

No declarations listed.