more Nat operations

Stdlib/Data/Nat.juvix

@@ -15,44 +15,24 @@ builtin nat-plus
 + (suc a) b := suc (a + b);
 
 infixl 7 *;
+builtin nat-mul
 * : Nat → Nat → Nat;
-* zero b := zero;
+* zero _ := zero;
 * (suc a) b := b + (a * b);
 
+builtin nat-sub
 sub : Nat → Nat → Nat;
 sub zero _ := zero;
 sub n zero := n;
 sub (suc n) (suc m) := sub n m;
 
+--terminating
+builtin nat-div
 div : Nat → Nat → Nat;
 div zero _ := zero;
 div n m := suc (div (sub n m) m);
 
-infixl 5 <=;
-<= : Nat → Nat → Bool;
-<= zero _ := true;
-<= _ zero := false;
-<= (suc n) (suc m) := n <= m;
-
-infixl 5 <;
-< : Nat → Nat → Bool;
-< n m := suc n <= m;
-
-infixl 5 >=;
->= : Nat → Nat → Bool;
->= n m := m <= n;
-
-infixl 5 >;
-> : Nat → Nat → Bool;
-> n m := m < n;
-
-infixl 5 ==;
-== : Nat → Nat → Bool;
-== zero zero := true;
-== zero _ := false;
-== _ zero := false;
-== (suc n) (suc m) := n == m;
-
+builtin nat-mod
 mod : Nat → Nat → Nat;
 mod n m := sub n ((div n m) * m);
 

Stdlib/Data/Nat/Ord.juvix

@@ -4,30 +4,35 @@ open import Stdlib.Data.Nat;
 open import Stdlib.Data.Ord;
 open import Stdlib.Data.Bool;
 
-compare : Nat → Nat → Ordering;
-compare zero zero := EQ;
-compare zero _ := LT;
-compare (suc _) zero := GT;
-compare (suc a) (suc b) := compare a b;
-
 infix 4 ==;
+builtin nat-eq
 == : Nat → Nat → Bool;
-== a b := isEQ (compare a b);
-
-infix 4 <;
-< : Nat → Nat → Bool;
-< a b := isLT (compare a b);
+== zero zero := true;
+== zero _ := false;
+== _ zero := false;
+== (suc n) (suc m) := n == m;
 
 infix 4 <=;
+builtin nat-le
 <= : Nat → Nat → Bool;
-<= a b := not (isGT (compare a b));
+<= zero _ := true;
+<= _ zero := false;
+<= (suc n) (suc m) := n <= m;
+
+infix 4 <;
+builtin nat-lt
+< : Nat → Nat → Bool;
+< n m := (suc n) <= m;
 
 infix 4 >;
 > : Nat → Nat → Bool;
-> a b := isGT (compare a b);
+> n m := m < n;
 
 infix 4 >=;
 >= : Nat → Nat → Bool;
->= a b := not (isLT (compare a b));
+>= n m := m <= n;
+
+compare : Nat → Nat → Ordering;
+compare n m := if (n == m) EQ (if (n < m) LT GT);
 
 end;