expected

Loading doc.disco...
Running tests...
  f: OK
Loaded.
type P = ℕ × ℕ

P is a type of stuff.

f : ℕ → ℕ

f is a function.
Some more documentation.

No documentation found for x.
~+~ : ℕ × ℕ → ℕ
precedence level 7, left associative

The sum of two numbers, types, or graphs.

https://disco-lang.readthedocs.io/en/latest/reference/addition.html

~! : ℕ → ℕ
precedence level 14

n! computes the factorial of n, that is, 1 * 2 * ... * n.

https://disco-lang.readthedocs.io/en/latest/reference/factorial.html

not~ : Bool → Bool
Alternative syntax: ¬~
precedence level 15

Logical negation: ¬true = false and ¬false = true.  Also written 'not'.

https://disco-lang.readthedocs.io/en/latest/reference/not.html