Skip to content

Native Documentation Tool

Inspired by Haddock and Agda, Juvix has its own documentation tool called Judoc.

Judoc is used to document parts of your code. You can attach Judoc blocks to the following entities:

  • A module.
  • A type definition.
  • A constructor definition.
  • A function definition.
  • An axiom definition.

In order to attach documentation to any of these entities, write blocks of documentation before them:

  1. For modules:
--- This module is cool
module Cool;
..
  • For type definitions:
--- Unary representation of natural numbers
type Nat : Type :=
  | --- Nullary constructor representing number 0
    zero : Nat
  | --- Unary constructor representing the successor of a natural number
    suc : Nat -> Nat;
  • For functions (and likewise for axioms):
--- The polymorphic identity function
id {A} (x : A) : A := x;

Block

A block can be one of:

  1. A paragraph.
  2. An example.

Blocks are separated by a line with only ---. For instance, this is a sequence of two blocks:

--- First block
---
--- Second block

Note that the following is a single block since it lacks the --- separator:

--- First block

--- Still first block

Alternatively, you can use block Judoc comments for that:

{-- First block

Second block
---}

Paragraph

A paragraph is a non-empty sequence of lines.

For instance, the following is a paragraph with two lines:

--- First line
--- Second line

Note that a rendered paragraph will have have no line breaks. If you want to have line breaks, you will need to split the paragraph. Hence, the paragraph above will be rendered as

First line Second line
Line

A line starts with --- and is followed by a non-empty sequence of atoms.

For instance, the following is a valid line:

--- A ;Pair Int Bool; contains an ;Int; and a ;Bool;
Atom

An atom is either:

  1. A string of text (including spaces but not line breaks).
  2. An inline Juvix expression surrounded by ;.

For instance, the following are valid atoms:

  1. I am some text.
  2. ;Pair Int Bool;

Example

--- >>> someExpression ;

The someExpression can span multiple lines and it must be ended with a ;. For instance:

--- >>> 1
        + 2
        + 3;

Comments