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

@[implicit_reducible]

instance Batteries.Util.instInhabitedLibraryNote : Inhabited LibraryNote

Equations

• Batteries.Util.instInhabitedLibraryNote = { default := Batteries.Util.instInhabitedLibraryNote._aux_1 }

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

@[implicit_reducible]

instance Batteries.Util.LibraryNote.instInhabitedLibraryNoteEntry : Inhabited LibraryNoteEntry

Equations

• Batteries.Util.LibraryNote.instInhabitedLibraryNoteEntry = { default := Batteries.Util.LibraryNote.instInhabitedLibraryNoteEntry._aux_1 }

def Batteries.Util.LibraryNote.encodeNameForExport (n : Lean.Name) : Lean.Name

Encode a name to be safe for the Lean export format.

The current export format (used by lean4export and consumed by external type checkers like nanoda_lib) does not support whitespace in declaration names. Library notes often have human-readable names with spaces like «my library note», which would produce declarations like LibraryNote.«my library note» that cannot be exported.

This function replaces spaces with underscores to produce export-safe names like LibraryNote.my_library_note.

Equations

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

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. (Note: spaces in the name are converted to underscores in the declaration name for compatibility with the Lean export format.) 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.