Disco allows special documentation comments, which
begin with three vertical bars (
|||) at the beginning of a line.
Anything written after
||| is documentation which will be attached
to the next definition (either a type definition or a
variable definition). This documentation can later
be accessed with the
:doc command. For example, suppose we have the
following in a file called
-- This is a comment that will be ignored. ||| f is a cool function which computes a thing. ||| It has two lines of documentation. f : N -> N f(x) = x + 7
Then at the disco prompt we can load the file, and see the
f using the
Disco> :load cool.disco Loading cool.disco... Loaded. Disco> :doc f f : ℕ → ℕ f is a cool function which computes a thing. It has two lines of documentation.