Documentation

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 cool.disco:

example/cool.disco

-- 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 documentation for f using the :doc command:

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.