HepLean Documentation

Batteries.Util.LibraryNote

Define the library_note command. #

source
def Batteries.Util.LibraryNote.LibraryNoteEntry :
Type

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

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

    Environment extension supporting library_note.

    source
    def Batteries.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. Use #help note "some tag" to display all notes with the tag "some tag" in the infoview. This command can be imported from Batteries.Tactic.HelpCmd .

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