'syntax' keyword (#64)

Stdlib/Data/Bool/Base.juvix

@@ -11,14 +11,14 @@ not : Bool → Bool;
 not true := false;
 not false := true;
 
-infixr 2 ||;
+syntax infixr 2 ||;
 --- Logical disjunction. Cannot be partially applied
 builtin bool-or
 || : Bool → Bool → Bool;
 || true _ := true;
 || false a := a;
 
-infixr 2 &&;
+syntax infixr 2 &&;
 --- Logical conjunction. Cannot be partially applied.
 builtin bool-and
 && : Bool → Bool → Bool;

Stdlib/Data/Int/Base.juvix

@@ -31,7 +31,7 @@ intSubNat m n :=
     | zero := ofNat (Nat.sub m n)
     | suc k := negSuc k;
 
-infixl 6 +;
+syntax infixl 6 +;
 --- Addition for ;Int;s.
 builtin int-plus
 + : Int -> Int -> Int;
@@ -52,7 +52,7 @@ neg : Int -> Int;
 neg (ofNat n) := negNat n;
 neg (negSuc n) := ofNat (suc n);
 
-infixl 7 *;
+syntax infixl 7 *;
 --- Multiplication for ;Int;s.
 builtin int-mul
 * : Int -> Int -> Int;
@@ -61,7 +61,7 @@ builtin int-mul
 * (negSuc m) (ofNat n) := negNat (suc m Nat.* n);
 * (negSuc m) (negSuc n) := ofNat (suc m Nat.* suc n);
 
-infixl 6 -;
+syntax infixl 6 -;
 --- Subtraction for ;Int;s.
 builtin int-sub
 - : Int -> Int -> Int;

Stdlib/Data/Int/Ord.juvix

@@ -6,37 +6,37 @@ open import Stdlib.Trait.Ord;
 
 import Stdlib.Data.Nat.Ord as Nat;
 
-infix 4 ==;
+syntax infix 4 ==;
 --- Tests for equality.
 builtin int-eq
 == : Int -> Int -> Bool;
 == (ofNat m) (ofNat n) := m Nat.== n;
 == (negSuc m) (negSuc n) := m Nat.== n;
 == _ _ := false;
 
-infix 4 /=;
+syntax infix 4 /=;
 --- Tests for inequality.
 /= : Int -> Int -> Bool;
 /= m n := not (m == n);
 
-infix 4 <=;
+syntax infix 4 <=;
 --- 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);
 
-infix 4 <;
+syntax infix 4 <;
 --- Returns ;true; iff the first element is less than the second.
 builtin int-lt
 < : Int -> Int -> Bool;
 < m n := m + 1 <= n;
 
-infix 4 >;
+syntax infix 4 >;
 --- Returns ;true; iff the first element is greater than the second.
 > : Int -> Int -> Bool;
 > m n := n < m;
 
-infix 4 >=;
+syntax infix 4 >=;
 --- Returns ;true; iff the first element is greater than or equal to the second.
 >= : Int -> Int -> Bool;
 >= m n := n <= m;

Stdlib/Data/List/Base.juvix

@@ -8,7 +8,7 @@ open import Stdlib.Trait.Ord;
 open import Stdlib.Data.Product.Base;
 open import Stdlib.Trait.Ord;
 
-infixr 5 ::;
+syntax infixr 5 ::;
 --- Inductive list.
 type List (a : Type) :=
   | --- The empty list
@@ -97,7 +97,7 @@ partition _ nil := nil, nil;
 partition f (x :: xs) :=
   if (f x) first second ((::) x) (partition f xs);
 
-infixr 5 ++;
+syntax infixr 5 ++;
 --- Concatenates two ;List;s.
 ++ : {A : Type} → List A → List A → List A;
 ++ nil ys := ys;

Stdlib/Data/Nat/Base.juvix

@@ -6,14 +6,14 @@ type Nat :=
   | zero : Nat
   | suc : Nat → Nat;
 
-infixl 6 +;
+syntax infixl 6 +;
 --- Addition for ;Nat;s.
 builtin nat-plus
 + : Nat → Nat → Nat;
 + zero b := b;
 + (suc a) b := suc (a + b);
 
-infixl 7 *;
+syntax infixl 7 *;
 --- Multiplication for ;Nat;s.
 builtin nat-mul
 * : Nat → Nat → Nat;

Stdlib/Data/Nat/Ord.juvix

@@ -4,7 +4,7 @@ open import Stdlib.Data.Nat.Base;
 open import Stdlib.Trait.Ord;
 open import Stdlib.Data.Bool;
 
-infix 4 ==;
+syntax infix 4 ==;
 --- Tests for equality.
 builtin nat-eq
 == : Nat → Nat → Bool;
@@ -13,31 +13,31 @@ builtin nat-eq
 == _ zero := false;
 == (suc n) (suc m) := n == m;
 
-infix 4 /=;
+syntax infix 4 /=;
 --- Tests for inequality.
 /= : Nat → Nat → Bool;
 /= x y := not (x == y);
 
-infix 4 <=;
+syntax infix 4 <=;
 --- Returns ;true; iff the first element is less than or equal to the second.
 builtin nat-le
 <= : Nat → Nat → Bool;
 <= zero _ := true;
 <= _ zero := false;
 <= (suc n) (suc m) := n <= m;
 
-infix 4 <;
+syntax infix 4 <;
 --- Returns ;true; iff the first element is less than the second.
 builtin nat-lt
 < : Nat → Nat → Bool;
 < n m := suc n <= m;
 
-infix 4 >;
+syntax infix 4 >;
 --- Returns ;true; iff the first element is greater than the second.
 > : Nat → Nat → Bool;
 > n m := m < n;
 
-infix 4 >=;
+syntax infix 4 >=;
 --- Returns ;true; iff the first element is greater than or equal to the second.
 >= : Nat → Nat → Bool;
 >= n m := m <= n;

Stdlib/Data/Product/Base.juvix

@@ -1,7 +1,7 @@
 module Stdlib.Data.Product.Base;
 
-infixr 2 ×;
-infixr 4 ,;
+syntax infixr 2 ×;
+syntax infixr 4 ,;
 --- Inductive pair. I.e. a tuple with two components.
 type × (A : Type) (B : Type) :=
   | , : A → B → A × B;

Stdlib/Data/String/Base.juvix

@@ -7,7 +7,7 @@ open import Stdlib.Function;
 builtin string
 axiom String : Type;
 
-infixr 5 ++str;
+syntax infixr 5 ++str;
 --- Concatenation of two ;String;s.
 builtin string-concat
 axiom ++str : String -> String -> String;

Stdlib/Data/String/Ord.juvix

@@ -3,7 +3,7 @@ module Stdlib.Data.String.Ord;
 open import Stdlib.Data.String.Base;
 open import Stdlib.Data.Bool;
 
-infix 4 ==;
+syntax infix 4 ==;
 --- Equality for ;String;s.
 builtin string-eq
 axiom == : String → String → Bool;

Stdlib/Function.juvix

@@ -3,7 +3,7 @@ module Stdlib.Function;
 open import Stdlib.Data.Nat.Base;
 open import Stdlib.Data.Product.Base;
 
-infixr 9 ∘;
+syntax infixr 9 ∘;
 --- Function composition.
 ∘ :
   {A : Type}
@@ -34,7 +34,7 @@ flip :
     → C;
 flip f b a := f a b;
 
-infixr 0 $;
+syntax infixr 0 $;
 --- Application operator with right associativity. Usually used as a syntactical
 --- facility.
 $ : {A : Type} → {B : Type} → (A → B) → A → B;
@@ -45,7 +45,7 @@ iterate : {A : Type} -> Nat -> (A -> A) -> A -> A;
 iterate zero _ a := a;
 iterate (suc n) f a := iterate n f (f a);
 
-infixl 0 on;
+syntax infixl 0 on;
 on :
   {A : Type}
     → {B : Type}
@@ -57,7 +57,7 @@ on :
     → C;
 on f g a b := f (g a) (g b);
 
-infixl 1 >>>;
+syntax infixl 1 >>>;
 builtin seq
 >>> : {A B : Type} → A → B → B;
 >>> x y := y;

Stdlib/System/IO.juvix

@@ -8,7 +8,7 @@ open import Stdlib.Data.Int using {Int};
 builtin IO
 axiom IO : Type;
 
-infixl 1 >>;
+syntax infixl 1 >>;
 builtin IO-sequence
 axiom >> : IO → IO → IO;