diff options
Diffstat (limited to 'transfer/examples/nat.tr')
| -rw-r--r-- | transfer/examples/nat.tr | 35 |
1 files changed, 17 insertions, 18 deletions
diff --git a/transfer/examples/nat.tr b/transfer/examples/nat.tr index f67dc55ce..cd9101574 100644 --- a/transfer/examples/nat.tr +++ b/transfer/examples/nat.tr @@ -1,23 +1,22 @@ -data Nat : Type where { - Zero : Nat ; - Succ : (n:Nat) -> Nat ; - } ; +data Nat : Type where + Zero : Nat + Succ : (n:Nat) -> Nat -plus : Nat -> Nat -> Nat ; -plus Zero y = y ; -plus (Succ x) y = Succ (plus x y) ; +plus : Nat -> Nat -> Nat +plus Zero y = y +plus (Succ x) y = Succ (plus x y) -pred : Nat -> Nat ; -pred Zero = Zero ; -pred (Succ n) = n ; +pred : Nat -> Nat +pred Zero = Zero +pred (Succ n) = n -natToInt : Nat -> Int ; -natToInt Zero = 0 ; -natToInt (Succ n) = 1 + natToInt n ; +natToInt : Nat -> Int +natToInt Zero = 0 +natToInt (Succ n) = 1 + natToInt n -plus : Nat -> Nat -> Nat ; -plus Zero y = y ; -plus (Succ x) y = Succ (plus x y) ; +plus : Nat -> Nat -> Nat +plus Zero y = y +plus (Succ x) y = Succ (plus x y) -intToNat : Int -> Nat ; -intToNat n = if n == 0 then Zero else Succ (intToNat (n-1)) ; +intToNat : Int -> Nat +intToNat n = if n == 0 then Zero else Succ (intToNat (n-1)) |