From 02c23401a7a3e54d48084fc2796a485de36383f1 Mon Sep 17 00:00:00 2001 From: bringert Date: Mon, 28 Nov 2005 21:45:22 +0000 Subject: Changed all example programs to use layout syntax. --- transfer/examples/nat.tr | 35 +++++++++++++++++------------------ 1 file changed, 17 insertions(+), 18 deletions(-) (limited to 'transfer/examples/nat.tr') 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)) -- cgit v1.2.3