implement argument lists for top-level definitions

1 files changed, 11 insertions, 10 deletions

diff --git a/test/bool.toytt b/test/bool.toytt
index c8e62fd..5f16d20 100644
--- a/test/bool.toytt
+++ b/test/bool.toytt
@@ -1,11 +1,13 @@
-def not : bool -> bool :=
-  \x -> bool-elim x at _ -> bool [
+def id (A : type) (x : A) : A := x
+
+def not (x : bool) : bool :=
+  bool-elim x at _ -> bool [
     true => false,
     false => true
   ]
 
-def and : bool -> bool -> bool :=
-  \x -> \y -> bool-elim x at _ -> bool [
+def and (x : bool) (y : bool) : bool :=
+  bool-elim x at _ -> bool [
     true => bool-elim y at _ -> bool [
       true => true,
       false => false
@@ -13,8 +15,8 @@ def and : bool -> bool -> bool :=
     false => false
   ]
 
-def or : bool -> bool -> bool :=
-  \x -> \y -> bool-elim x at _ -> bool [
+def or (x : bool) (y : bool) : bool :=
+  bool-elim x at _ -> bool [
     true => true,
     false => bool-elim y at _ -> bool [
       true => true,
@@ -22,7 +24,6 @@ def or : bool -> bool -> bool :=
     ]
   ]
 
-def xor : bool -> bool -> bool :=
-  \x -> \y -> or
-    (and x (not y))
-	(and (not x) y)
+def xor (x : bool) (y : bool) : bool :=
+  or (and x (not y))
+     (and (not x) y)