Documentation

Std.Util.LibraryNote

Define the library_note command. #

A library note consists of a (short) tag and a (long) note.

Instances For
    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.

    Instances For