tur/nat
stdlib/nat.tur
natural numbers as a sum: Zero and Succ.
Nat encodes a number at the type level as a phantom type. True compile-time length safety is deferred to a future dependent-types phase.
Since: Phase G4
defdata
Nat
(defdata Nat (Zero) (Succ Nat))
defn
nat-zero
(nat-zero :Nat)
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] :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] :int)
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] :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