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
      instance Batteries.Util.LibraryNote.instLibraryNoteEntryInhabited :
      Inhabited LibraryNoteEntry
      Equations
        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
          Instances For