tur/nat
stdlib/nat.tur
type-level natural numbers via GADT for phantom length annotations.
Since: Phase G4
defgadt
Nat
(defgadt Nat (Zero) (Nat) (Succ) (Nat) (Nat))
defn
nat-zero
(nat-zero :)
construct the Zero natural number.
Returns
A (Nat) value representing zero.
Example
(nat-zero) ; => Zero
Since: Phase G4
defn
nat-succ
(nat-succ [n : Nat] :)
construct the successor of a natural number.
Parameters
| n | the predecessor (Nat) value |
Returns
A (Nat) value representing n+1.
Example
(nat-succ (nat-zero)) ; => Succ(Zero)
Since: Phase G4
defn
nat-to-int
(nat-to-int [n : Nat] :)
convert a type-level Nat to a runtime integer.
Parameters
| n | the (Nat) value to convert |
Returns
The integer representation of n.
Example
(nat-to-int (Succ (Succ (Zero)))) ; => 2
Since: Phase G4
defn
nat-add
(nat-add [a : Nat b : Nat] :)
add two type-level Nat values.
Parameters
| a | first (Nat) value | |
| b | second (Nat) value |
Returns
A (Nat) representing a + b.
Example
(nat-to-int (nat-add (Succ (Zero)) (Succ (Succ (Zero))))) ; => 3
Since: Phase G4