Fixed grammar and more peano stuff

Grammar.cf

@@ -1,3 +1,10 @@
+
+-------------------------------------------------------------------------------
+-- * PROGRAM
+-------------------------------------------------------------------------------
+
+Program. Program ::= [Def];
+
 -------------------------------------------------------------------------------
 -- * TOP-LEVEL
 -------------------------------------------------------------------------------
@@ -101,3 +108,4 @@ token Symbol (["@#%^&*_-+=|?/<>,•:[]"]+) ;
 
 comment "--";
 comment "{-" "-}";
+

test_program.crf

@@ -3,14 +3,8 @@ data Nat where
   Zero : Nat
   Succ : Nat -> Nat
 
-toInt : Nat -> Int
+-- Returns 10_000
-toInt a = case a of
+main = toInt (fromInt 10000)
-    Succ n => 1 + toInt n
-    Zero => 0
-
-fromInt a = case a of
-    0 => Zero
-    n => Succ (fromInt (a - 1))
 
 -- Peano arithmetic --
 
@@ -26,5 +20,40 @@ mul left right = case right of
     Zero => Zero
     Succ n => add left (mul left n)
 
--- Returns 10_000
+eq : Nat -> Nat -> Nat
-main = toInt (mul (fromInt 100) (fromInt 100))
+eq a b = case a of
+    Zero => case b of 
+        Zero => Succ Zero
+        _    => Zero
+    Succ n => case b of
+        Zero => Zero
+        Succ m => eq n m
+
+less : Nat -> Nat -> Nat
+less a b = case a of
+    Zero => case b of
+        Zero => Zero
+        Succ n => Succ Zero
+    Succ n => case b of
+        Zero => Zero
+        Succ m => less n m
+
+greater : Nat -> Nat -> Nat
+greater a b = case b of
+    Zero => case a of
+        Zero => Zero
+        Succ n => Succ Zero
+    Succ n => case a of
+        Zero => Zero
+        Succ m => less n m
+
+-- Aux
+
+toInt : Nat -> Int
+toInt a = case a of
+    Succ n => 1 + toInt n
+    Zero => 0
+
+fromInt a = case a of
+    0 => Zero
+    n => Succ (fromInt (a - 1))