Documentation

Std.Util.LibraryNote

Define the library_note command. #

source
def Std.Util.LibraryNote.LibraryNoteEntry :
Type

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

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

    Environment extension supporting library_note.

    source
    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.
    Instances For