Define the library_note command.

def Batteries.Util.LibraryNote : Type

A library note is identified by the name of its declaration, and its content should be contained in its doc-string.

Equations

• Batteries.Util.LibraryNote = Unit

instance Batteries.Util.instInhabitedLibraryNote : Inhabited LibraryNote

Equations

• Batteries.Util.instInhabitedLibraryNote = instInhabitedPUnit

def Batteries.Util.LibraryNote.LibraryNoteEntry : Type

Entry for library notes in the environment extension.

We only store the name, and look up the constant's docstring to find its contents.

Equations

• Batteries.Util.LibraryNote.LibraryNoteEntry = Lean.Name

instance Batteries.Util.LibraryNote.instInhabitedLibraryNoteEntry : Inhabited LibraryNoteEntry

Equations

• Batteries.Util.LibraryNote.instInhabitedLibraryNoteEntry = Lean.instInhabitedName

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

Environment extension supporting library_note.

def Batteries.Util.LibraryNote.commandLibrary_note___ : Lean.ParserDescr

library_note «my note» /-- documentation -/ creates a library note named my note in the LibraryNote namespace, whose content is /-- documentation -/. This can then be cross-referenced using

-- See note [some tag]

in doc-comments. You can access the contents using, for example, #print LibraryNote.«my note». 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.

def Batteries.Util.LibraryNote.commandLibrary_note____1 : Lean.ParserDescr

Support the old library_note "foo" syntax, with a deprecation warning.

Equations

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

def Batteries.Util.LibraryNote.commandLibrary_note2___ : Lean.ParserDescr

Support the old library_note2 «foo» syntax, with a deprecation warning.

Equations

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

def Batteries.Util.LibraryNote.commandLibrary_note2____1 : Lean.ParserDescr

Support the old library_note2 "foo" syntax, with a deprecation warning.

Equations

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