diff options
| author | bringert <bringert@cs.chalmers.se> | 2005-11-28 21:45:22 +0000 |
|---|---|---|
| committer | bringert <bringert@cs.chalmers.se> | 2005-11-28 21:45:22 +0000 |
| commit | 02c23401a7a3e54d48084fc2796a485de36383f1 (patch) | |
| tree | 03574e9f1c862f2b5685741c6c9d8ee8029aea21 /transfer/examples/nat.tr | |
| parent | 5a82068ddc0e75ee2f2280ffb5da9cda3e53bac3 (diff) | |
Changed all example programs to use layout syntax.
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)) |