Remove old function syntax

Stdlib/Data/Bool/Base.juvix

@@ -36,9 +36,7 @@ if : {A : Type} → Bool → A → A → A
   | false _ b := b;
 
 --- Logical disjunction.
-or : Bool → Bool → Bool
-  | a b := a || b;
+or (a b : Bool) : Bool := a || b;
 
 --- Logical conjunction.
-and : Bool → Bool → Bool
-  | a b := a && b;
+and (a b : Bool) : Bool := a && b;

Stdlib/Data/Int/Base.juvix

@@ -27,11 +27,10 @@ nonNeg : Int -> Bool
 
 --- Subtraction for ;Nat;s.
 builtin int-sub-nat
-intSubNat : Nat -> Nat -> Int
-  | m n :=
-    case sub n m
-      | zero := ofNat (Nat.sub m n)
-      | suc k := negSuc k;
+intSubNat (n m : Nat) : Int :=
+  case sub n m
+    | zero := ofNat (Nat.sub m n)
+    | suc k := negSuc k;
 
 syntax operator + additive;
 
@@ -69,8 +68,7 @@ syntax operator - additive;
 
 --- Subtraction for ;Int;s.
 builtin int-sub
-- : Int -> Int -> Int
-  | m n := m + neg n;
+- (n m : Int) : Int := m + neg n;
 
 --- Division for ;Int;s.
 builtin int-div

Stdlib/Data/Int/Ord.juvix

@@ -20,43 +20,36 @@ builtin int-eq
 syntax operator /= comparison;
 
 --- Tests for inequality.
-/= : Int -> Int -> Bool
-  | m n := not (m == n);
+/= (m n : Int) : Bool := not (m == n);
 
 syntax operator <= comparison;
 
 --- Returns ;true; iff the first element is less than or equal to the second.
 builtin int-le
-<= : Int -> Int -> Bool
-  | m n := nonNeg (n - m);
+<= (m n : Int) : Bool := nonNeg (n - m);
 
 syntax operator < comparison;
 
 --- Returns ;true; iff the first element is less than the second.
 builtin int-lt
-< : Int -> Int -> Bool
-  | m n := m + 1 <= n;
+< (m n : Int) : Bool := m + 1 <= n;
 
 syntax operator > comparison;
 
 --- Returns ;true; iff the first element is greater than the second.
-> : Int -> Int -> Bool
-  | m n := n < m;
+> (m n : Int) : Bool := n < m;
 
 syntax operator >= comparison;
 
 --- Returns ;true; iff the first element is greater than or equal to the second.
->= : Int -> Int -> Bool
-  | m n := n <= m;
+>= (m n : Int) : Bool := n <= m;
 
 --- Tests for ;Ordering;.
-compare : Int -> Int -> Ordering
-  | m n := if (m == n) EQ (if (m < n) LT GT);
+compare (m n : Int) : Ordering :=
+  if (m == n) EQ (if (m < n) LT GT);
 
 --- Returns the smallest ;Int;.
-min : Int → Int → Int
-  | x y := if (x < y) x y;
+min (x y : Int) : Int := if (x < y) x y;
 
 --- Returns the biggest ;Int;.
-max : Int → Int → Int
-  | x y := if (x > y) x y;
+max (x y : Int) : Int := if (x > y) x y;

Stdlib/Data/Int/Range.juvix

@@ -17,20 +17,18 @@ type Range :=
 syntax iterator for {init: 1, range: 1};
 
 {-# specialize: [1, 3] #-}
-for : {A : Type} → (A → Int → A) → A → Range → A
-  | {A} f a mkRange@{low; high; step} :=
+for {A} (f : A → Int → A) (a : A) : Range → A
+  | mkRange@{low; high; step} :=
     let
       terminating
-      go : A → Int → A;
-      go acc n := if (n > high) acc (go (f acc n) (n + step));
+      go (acc : A) (n : Int) : A :=
+        if (n > high) acc (go (f acc n) (n + step));
     in go a low;
 
 syntax operator to range;
 
-to : Int → Int → Range
-  | l h := mkRange l h 1;
+to (l h : Int) : Range := mkRange l h 1;
 
 syntax operator step step;
 
-step : Range → Int → Range
-  | r s := r @Range{step := s};
+step (r : Range) (s : Int) : Range := r@Range{step := s};

Stdlib/Data/List.juvix

@@ -15,41 +15,41 @@ import Stdlib.Trait.Show as Show;
 open Show using {Show};
 
 --- 𝒪(1). Partial function that returns the first element of a ;List;.
-head : {A : Type} → List A → A
+head {A} : List A → A
   | (x :: _) := x
   | nil := fail "head: empty list";
 
 module ListTraits;
-  Eq : {A : Type} -> Eq.Eq A -> Eq.Eq (List A)
-    | {A} (Eq.mkEq eq-a) :=
+  Eq {A} : Eq.Eq A -> Eq.Eq (List A)
+    | (Eq.mkEq eq-a) :=
       let
-        go : List A -> List A -> Bool;
-        go nil nil := true;
-        go nil _ := false;
-        go _ nil := false;
-        go (x :: xs) (y :: ys) := if (eq-a x y) (go xs ys) false;
+        go : List A -> List A -> Bool
+          | nil nil := true
+          | nil _ := false
+          | _ nil := false
+          | (x :: xs) (y :: ys) := if (eq-a x y) (go xs ys) false;
       in Eq.mkEq go;
 
-  Ord : {A : Type} -> Ord.Ord A -> Ord.Ord (List A)
-    | {A} (Ord.mkOrd cmp-a) :=
+  Ord {A} : Ord.Ord A -> Ord.Ord (List A)
+    | (Ord.mkOrd cmp-a) :=
       let
-        go : List A -> List A -> Ord.Ordering;
-        go nil nil := Ord.EQ;
-        go nil _ := Ord.LT;
-        go _ nil := Ord.GT;
-        go (x :: xs) (y :: ys) :=
-          case cmp-a x y
-            | Ord.LT := Ord.LT
-            | Ord.GT := Ord.GT
-            | Ord.EQ := go xs ys;
+        go : List A -> List A -> Ord.Ordering
+          | nil nil := Ord.EQ
+          | nil _ := Ord.LT
+          | _ nil := Ord.GT
+          | (x :: xs) (y :: ys) :=
+            case cmp-a x y
+              | Ord.LT := Ord.LT
+              | Ord.GT := Ord.GT
+              | Ord.EQ := go xs ys;
       in Ord.mkOrd go;
 
-  Show : {A : Type} -> Show.Show A -> Show.Show (List A)
-    | {A} (Show.mkShow to-str) :=
+  Show {A} : Show.Show A -> Show.Show (List A)
+    | (Show.mkShow to-str) :=
       let
-        go : List A -> String;
-        go nil := "nil";
-        go (x :: xs) := to-str x ++str " :: " ++str go xs;
+        go : List A -> String
+          | nil := "nil"
+          | (x :: xs) := to-str x ++str " :: " ++str go xs;
       in Show.mkShow
         λ {
           | nil := "nil"