Documentation

Std.Util.LibraryNote

Define the library_note command. #

source
ink
def Std.Util.LibraryNote.LibraryNoteEntry :
Type

A library note consists of a (short) tag and a (long) note.

Equations
source
ink
opaque Std.Util.LibraryNote.libraryNoteExt :
Lean.SimplePersistentEnvExtension Std.Util.LibraryNote.LibraryNoteEntry (Array Std.Util.LibraryNote.LibraryNoteEntry)

Environment extension supporting library_note.

source
ink
def Std.Util.LibraryNote.commandLibrary_note___ :
Lean.ParserDescr
library_note "some tag" /--
... some explanation ...
-/

creates a new "library note", which can then be cross-referenced using

-- See note [some tag]

in doc-comments.

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