(* Text inserted between matching "(*" and "*)" is comment and should be
   ignored by your interpreter. *)

(* There are five examples in this input file, each terminated with a
   a semi-colon. The first 3 should cause no error. *)

(*************************************************************************)

(lambda fst: Nat -> Nat. (lambda snd: Bool. fst)) (lambda var: Nat. var) true;

(lambda x: Nat. succ x) 0;

pred ((lambda x: Nat. if (iszero x) then (succ x) else x) 0) ;

(* the next example should cause a syntactic error, not related to types. *)

(lambda x:Nat. lambda y:Bool. ) (lambda x:Nat.x);

(* the next example should cause a type-checking error. *)

(lambda x:Nat. lambda y:Bool. x) (lambda x:Nat. x);