commandLibrary_note2___ — Mathlib

Lean4
/-- `library_note2 «my note» /-- documentation -/` creates a library note named `my note`
in the `Mathlib.LibraryNote` namespace, whose content is `/-- documentation -/`.
You can access this note using, for example, `#print Mathlib.LibraryNote.«my note»`.
-/
@[command_parser 1000]
public meta def commandLibrary_note2___ : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `commandLibrary_note2___ 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "library_note2 ") (ParserDescr.const✝ `ident))
        (ParserDescr.unary✝ `group (ParserDescr.const✝ `ppSpace)))
      (ParserDescr.const✝ `docComment))
Похожие утверждения