doc: moduleDoc

leanprover · Apr 10, 2024 · db9ba88 · db9ba88
1 parent e41cd31
commit db9ba88
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
@@ -44,6 +44,11 @@ match against a quotation in a command kind's elaborator). -/
 @[builtin_term_parser low] def quot := leading_parser
   "`(" >> withoutPosition (incQuotDepth (many1Unbox commandParser)) >> ")"
 
+/--
+`/-! <text> -/` defines a *module docstring* that can be displayed by documentation generation
+tools. The string is associated with the corresponding position in the file. It can be used
+multiple times in the same file.
+-/
 @[builtin_command_parser]
 def moduleDoc := leading_parser ppDedent <|
   "/-!" >> commentBody >> ppLine