Documentation

Batteries.Util.LibraryNote

Define the library_note command. #

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.