diff --git a/test.hm b/test.hm index adf26ac..c0c89d1 100644 --- a/test.hm +++ b/test.hm @@ -6,7 +6,6 @@ type Nat -- 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))