Define the library_note command. #
A library note consists of a (short) tag and a (long) note.
Instances For
Environment extension supporting library_note.
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.