replace all remaining ≔ by :=

Stdlib/Data/Bool.juvix

@@ -6,21 +6,21 @@ inductive Bool {
 };
 
 not : Bool → Bool;
-not true ≔ false;
-not false ≔ true;
+not true := false;
+not false := true;
 
 infixr 2 ||;
 || : Bool → Bool → Bool;
-|| false a ≔ a;
-|| true _ ≔ true;
+|| false a := a;
+|| true _ := true;
 
 infixr 2 &&;
 && : Bool → Bool → Bool;
-&& false _ ≔ false;
-&& true a ≔ a;
+&& false _ := false;
+&& true a := a;
 
 if : {A : Type} → Bool → A → A → A;
-if true a _ ≔ a;
+if true a _ := a;
 if false _ b := b;
 
 --------------------------------------------------------------------------------

Stdlib/Data/List.juvix

@@ -13,92 +13,92 @@ inductive List (a : Type) {
 };
 
 elem : {A : Type} → (A → A → Bool) → A → List A → Bool;
-elem _ _ nil ≔ false;
-elem eq s (x ∷ xs) ≔ eq s x || elem eq s xs;
+elem _ _ nil := false;
+elem eq s (x ∷ xs) := eq s x || elem eq s xs;
 
 foldr : {A : Type} → {B : Type} → (A → B → B) → B → List A → B;
-foldr _ z nil ≔ z;
-foldr f z (h ∷ hs) ≔ f h (foldr f z hs);
+foldr _ z nil := z;
+foldr f z (h ∷ hs) := f h (foldr f z hs);
 
 foldl : {A : Type} → {B : Type} → (B → A → B) → B → List A → B;
-foldl f z nil ≔ z ;
-foldl f z (h ∷ hs) ≔ foldl f (f z h) hs;
+foldl f z nil := z ;
+foldl f z (h ∷ hs) := foldl f (f z h) hs;
 
 map : {A : Type} → {B : Type} → (A → B) → List A → List B;
-map f nil ≔ nil;
-map f (h ∷ hs) ≔ f h ∷ map f hs;
+map f nil := nil;
+map f (h ∷ hs) := f h ∷ map f hs;
 
 filter : {A : Type} → (A → Bool) → List A → List A;
-filter _ nil ≔ nil;
-filter f (h ∷ hs) ≔ if (f h)
+filter _ nil := nil;
+filter f (h ∷ hs) := if (f h)
    (h ∷ filter f hs)
    (filter f hs);
 
 length : {A : Type} → List A → Nat;
-length nil ≔ zero;
-length (_ ∷ l) ≔ suc (length l);
+length nil := zero;
+length (_ ∷ l) := suc (length l);
 
 reverse : {A : Type} → List A → List A;
-reverse ≔ foldl (flip (∷)) nil;
+reverse := foldl (flip (∷)) nil;
 
 replicate : {A : Type} → Nat → A → List A;
-replicate zero _ ≔ nil;
-replicate (suc n) x ≔  x ∷ replicate n x;
+replicate zero _ := nil;
+replicate (suc n) x :=  x ∷ replicate n x;
 
 take : {A : Type} → Nat → List A → List A;
-take (suc n) (x ∷ xs) ≔ x ∷ take n xs;
-take _ _ ≔ nil;
+take (suc n) (x ∷ xs) := x ∷ take n xs;
+take _ _ := nil;
 
 splitAt : {A : Type} → Nat → List A → List A × List A;
-splitAt _ nil ≔ nil , nil ;
-splitAt zero xs ≔  nil , xs;
-splitAt (suc zero) (x ∷ xs) ≔ x ∷ nil , xs;
-splitAt (suc (suc m)) (x ∷ xs) ≔ first ((∷) x) (splitAt m xs);
+splitAt _ nil := nil , nil ;
+splitAt zero xs :=  nil , xs;
+splitAt (suc zero) (x ∷ xs) := x ∷ nil , xs;
+splitAt (suc (suc m)) (x ∷ xs) := first ((∷) x) (splitAt m xs);
 
 merge : {A : Type} → (A → A → Ordering) → List A → List A → List A;
-merge cmp (x ∷ xs) (y ∷ ys) ≔
+merge cmp (x ∷ xs) (y ∷ ys) :=
    if (isLT (cmp x y))
     (x ∷ merge cmp xs (y ∷ ys))
     (y ∷ merge cmp (x ∷ xs) ys);
-merge _ nil ys ≔ ys;
-merge _ xs nil ≔ xs;
+merge _ nil ys := ys;
+merge _ xs nil := xs;
 
 partition : {A : Type} → (A → Bool) → List A → List A × List A;
-partition _ nil ≔ nil , nil ;
-partition f (x ∷ xs) ≔ (if (f x) first second) ((∷) x) (partition f xs);
+partition _ nil := nil , nil ;
+partition f (x ∷ xs) := (if (f x) first second) ((∷) x) (partition f xs);
 
 infixr 5 ++;
 ++ : {A : Type} → List A → List A → List A;
-++ nil ys ≔ ys;
-++ (x ∷ xs) ys ≔ x ∷ (xs ++ ys);
+++ nil ys := ys;
+++ (x ∷ xs) ys := x ∷ (xs ++ ys);
 
 flatten : {A : Type} → List (List A) → List A;
-flatten ≔ foldl (++) nil;
+flatten := foldl (++) nil;
 
 prependToAll : {A : Type} → A → List A → List A;
-prependToAll _ nil ≔ nil;
-prependToAll sep (x ∷ xs) ≔ sep ∷ x ∷ prependToAll sep xs;
+prependToAll _ nil := nil;
+prependToAll sep (x ∷ xs) := sep ∷ x ∷ prependToAll sep xs;
 
 intersperse : {A : Type} → A → List A → List A;
-intersperse _ nil ≔ nil;
-intersperse sep (x ∷ xs) ≔ x ∷ prependToAll sep xs;
+intersperse _ nil := nil;
+intersperse sep (x ∷ xs) := x ∷ prependToAll sep xs;
 
 head : {A : Type} → List A → A;
-head (x ∷ _) ≔ x;
+head (x ∷ _) := x;
 
 tail : {A : Type} → List A → List A;
-tail (_ ∷ xs) ≔ xs;
+tail (_ ∷ xs) := xs;
 
 terminating
 transpose : {A : Type} → List (List A) → List (List A);
-transpose (nil ∷ _) ≔ nil;
-transpose xss ≔ (map head xss) ∷ (transpose (map tail xss));
+transpose (nil ∷ _) := nil;
+transpose xss := (map head xss) ∷ (transpose (map tail xss));
 
 any : {A : Type} → (A → Bool) → List A → Bool;
-any f xs ≔ foldl (||) false (map f xs);
+any f xs := foldl (||) false (map f xs);
 
 null : {A : Type} → List A → Bool;
-null nil ≔ true;
-null _ ≔ false;
+null nil := true;
+null _ := false;
 
 end;

Stdlib/Data/List/Ord.juvix

@@ -4,10 +4,10 @@ open import Stdlib.Data.Ord;
 open import Stdlib.Data.List;
 
 compare : {A : Type} → (A → A → Ordering) → List A → List A → Ordering;
-compare _ nil nil ≔ EQ;
-compare _ nil (_ ∷ _) ≔ LT;
-compare _ (_ ∷ _) nil ≔ GT;
-compare cmp (x ∷ xs) (y ∷ ys) ≔ ifOrd (cmp x y)
+compare _ nil nil := EQ;
+compare _ nil (_ ∷ _) := LT;
+compare _ (_ ∷ _) nil := GT;
+compare cmp (x ∷ xs) (y ∷ ys) := ifOrd (cmp x y)
   LT
   (compare cmp xs ys)
   GT;

Stdlib/Data/Nat.juvix

@@ -20,31 +20,31 @@ infixl 7 *;
 * (suc a) b := b + (a * b);
 
 one : Nat;
-one ≔ suc zero;
+one := suc zero;
 
 two : Nat;
-two ≔ suc one;
+two := suc one;
 
 three : Nat;
-three ≔ suc two;
+three := suc two;
 
 four : Nat;
-four ≔ suc three;
+four := suc three;
 
 five : Nat;
-five ≔ suc four;
+five := suc four;
 
 six : Nat;
-six ≔ suc five;
+six := suc five;
 
 seven : Nat;
-seven ≔ suc six;
+seven := suc six;
 
 eight : Nat;
-eight ≔ suc seven;
+eight := suc seven;
 
 nine : Nat;
-nine ≔ suc eight;
+nine := suc eight;
 
 axiom natToStr : Nat → String;
 compile natToStr {

Stdlib/Data/Nat/Ord.juvix

@@ -5,9 +5,9 @@ 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 zero zero := EQ;
+compare zero _ := LT;
+compare (suc _) zero := GT;
 compare (suc a) (suc b) := compare a b;
 
 infix 4 ==;

Stdlib/Data/Ord.juvix

@@ -9,20 +9,20 @@ inductive Ordering {
 };
 
 isLT : Ordering → Bool;
-isLT LT ≔ true;
-isLT _ ≔ false;
+isLT LT := true;
+isLT _ := false;
 
 isEQ : Ordering → Bool;
-isEQ EQ ≔ true;
-isEQ _ ≔ false;
+isEQ EQ := true;
+isEQ _ := false;
 
 isGT : Ordering → Bool;
-isGT GT ≔ true;
-isGT _ ≔ false;
+isGT GT := true;
+isGT _ := false;
 
 ifOrd : {A : Type} → Ordering -> A → A → A → A;
-ifOrd LT lt eq gt ≔ lt;
-ifOrd EQ lt eq gt ≔ eq;
-ifOrd GT lt eq gt ≔ gt;
+ifOrd LT lt eq gt := lt;
+ifOrd EQ lt eq gt := eq;
+ifOrd GT lt eq gt := gt;
 
 end;

Stdlib/Data/Product.juvix

@@ -10,7 +10,7 @@ uncurry : {A : Type} → {B : Type} → {C : Type} → (A → B → C) → A ×
 uncurry f (a , b) := f a b;
 
 fst : {A : Type} → {B : Type} → A × B → A;
-fst (a , _) ≔ a;
+fst (a , _) := a;
 
 snd : {A : Type} → {B : Type} → A × B → B;
 snd (_ , b) := b;

Stdlib/Function.juvix

@@ -2,20 +2,20 @@ module Stdlib.Function;
 
 infixr 9 ∘;
 ∘ : {A : Type} → {B : Type} → {C : Type} → (B → C) → (A → B) → A → C;
-∘ f g x ≔ f (g x);
+∘ f g x := f (g x);
 
 const : {A : Type} → {B : Type} → A → B → A;
-const a _ ≔ a;
+const a _ := a;
 
 id : {A : Type} → A → A;
-id a ≔ a;
+id a := a;
 
 flip : {A : Type} → {B : Type} → {C : Type} → (A → B → C) → B → A → C;
 flip f b a := f a b;
 
 infixr 0 $;
 $ : {A : Type} → {B : Type} → (A → B) → A → B;
-$ f x ≔ f x;
+$ f x := f x;
 
 infixl 0 on;
 on : {A : Type} → {B : Type} → {C : Type} → (B -> B -> C) -> (A -> B) -> A -> A -> C;