mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-09 04:59:31 -06:00
25 lines
451 B
Plaintext
25 lines
451 B
Plaintext
import prelude
|
|
|
|
data Nat : Type where
|
|
Zero : Nat
|
|
Succ : (n:Nat) -> Nat
|
|
|
|
add_Nat : Add Nat
|
|
add_Nat = rec zero = Zero
|
|
plus = natPlus
|
|
|
|
natPlus : Nat -> Nat -> Nat
|
|
natPlus Zero y = y
|
|
natPlus (Succ x) y = Succ (natPlus x y)
|
|
|
|
pred : Nat -> Nat
|
|
pred Zero = Zero
|
|
pred (Succ n) = n
|
|
|
|
natToInt : Nat -> Integer
|
|
natToInt Zero = 0
|
|
natToInt (Succ n) = 1 + natToInt n
|
|
|
|
intToNat : Integer -> Nat
|
|
intToNat n = if n == 0 then Zero else Succ (intToNat (n-1))
|