fixed test up a bit

test.hm

@@ -1,49 +1,32 @@
--- currently all parameterised types are commented out until kinds are being implemented
+-- one could define the naturals as follows
-
--- no pattern matching, instead a recursor is given based on your inductive definition
--- for example: the following
-
-{-
-type List A
-  | nil : List A
-  |	cons  : A → List A → List A
--}
-
--- will bring the following into scope
--- rec[List] : B → (A → B → B) → List A → B
-
--- map could then be written as
- 
-{-
-map : (A → B) → List A → List B
- := rec[List] nil (λx xs. cons (f x) xs)
--}
-
--- one could then define the naturals as follows
-
 type Nat
   | zero : Nat
   | succ : Nat → Nat
 
--- defining addition as
+-- which will bring a recursor for the type into scope
+-- rec[Nat] : A → (A → A) → Nat → A
 
+
+-- defining addition as
 add : Nat → Nat → Nat
  := rec[Nat] (λx. x) (λf n. succ (f n))
 
--- since                | rec[Nat] : B → (Nat → B → B) → Nat → B
+-- since                | rec[Nat] : A → (A → A) → Nat → A
--- which generalizes to | rec[Nat] : (Nat → Nat) → (Nat → (Nat → Nat) → (Nat → Nat)) → Nat → Nat → Nat
+-- which generalizes to | rec[Nat] : (Nat → Nat) → ((Nat → Nat) → (Nat → Nat)) → Nat → (Nat → Nat)
 --                                   ^ adding 0    ^ recursively adding one more       ^ resulting addition type
 
 -- id is used to not add anything, the second function takes the last addition function and adds a layer
 -- of succ onto it, this way it generates a function for adding the right amount.
 
--- multiplication is defined similairly
 
+
+-- multiplication is defined similairly
 mul : Nat → Nat → Nat
  := rec[Nat] (λx. zero) (λf n. add n (f n))
 
--- here's an example of a simpler type
 
+
+-- here's an example of a simpler type
 type Bool
   | true : Bool
   | false : Bool
@@ -52,14 +35,19 @@ not : Bool → Bool
  := rec[Bool] false true
 
 -- now, let's look at a bit more interesting example
-
 type Expr
   | ENat : Nat →  Expr
   | EAdd : Expr → Expr → Expr
   | EMul : Expr → Expr → Expr
 
 -- this generates the following recursor
--- rec[Expr] : (Nat → B) → (B → B → B) → (B → B → B) → Expr → B
+-- rec[Expr] : (Nat → A) → (A → A → A) → (A → A → A) → Expr → A
+
+
 
 eval : Expr → Nat
  := rec[Expr] (λx. x) add mul
+
+-- here's some other functions
+isEven : Nat → Bool
+ := rec[Nat] true not