# 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

- Batteries.Util.LibraryNote.LibraryNoteEntry = (String × String)

Instances For

source
instance Batteries.Util.LibraryNote.instInhabitedLibraryNoteEntry :
Inhabited LibraryNoteEntry
Equations

- Batteries.Util.LibraryNote.instInhabitedLibraryNoteEntry = instInhabitedProd

source
opaque Batteries.Util.LibraryNote.libraryNoteExt :
Lean.SimplePersistentEnvExtension LibraryNoteEntry (Array 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