Define the library_note command.

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)

opaque Batteries.Util.LibraryNote.libraryNoteExt : Lean.SimplePersistentEnvExtension Batteries.Util.LibraryNote.LibraryNoteEntry (Array Batteries.Util.LibraryNote.LibraryNoteEntry)

Environment extension supporting library_note.

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.

Equations

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