DATA Expr
   | Variable
	      ident : Identifier
	 | Apply
	      function : Expr,
				argument : Expr
	 | Lambda
	      ident : Identifier,   
        body : Expr

{- 
  Can I have some comments please
-}
	
JUDGEMENT Gamma |- Expr : Type;
				
RULE
   
------------------------- [Var]
   G |- Variable x : a;
   
instc a (mylookup x G) "Should not fail"

RULE

   G |- e1 : t1;
   G |- e2 : t2;
------------------------- [App]
   G |- Apply e1 e2 : a;

eqc t1 (arrow t2 a) "Inconsistent types in application"

RULE

   update x b G |- e : t;
-------------------------- [Abs]
   G |- Lambda x e : a;
   
eqc a (arrow b t) "Inconsistent types in lambda abstraction"

DATA Expr
   | Let
	     ident : Identifier,
			 decl : Expr,
			 body : Expr
   | Where
			 body : Expr,
	     ident : Identifier,
			 definition : Expr

RULE

   G |- e1 : t1;
   update x s G |- e2 : t2;
---------------------------- [Let]
   G |- Let x e1 e2 : a;
 
genc s G t1 "Generalize failed in Let",
eqc t2 a "Type of body does not match context type for Let"

RULE
   G |- e2 : t2;
   update x s G |- e1 : t1;
---------------------------- [Where]
   G |- Where e1 x e2 : a;

genc s G t2 "Generalize failed in Where",
eqc t1 a "Type of body does not match type of Where"

MACRO
   Let x e1 e2 => Where e2 x e1