Rplace ≔ by :=

Stdlib/Data/Bool.juvix

@@ -21,7 +21,7 @@ infixr 2 &&;
 
 if : {A : Type} → Bool → A → A → A;
 if true a _ ≔ a;
-if false _ b ≔ b;
+if false _ b := b;
 
 --------------------------------------------------------------------------------
 -- Backend Booleans
@@ -61,6 +61,6 @@ compile bool {
 };
 
 from-backend-bool : BackendBool → Bool;
-from-backend-bool bb ≔ bool bb true false;
+from-backend-bool bb := bool bb true false;
 
 end;

Stdlib/Data/List.juvix

@@ -34,22 +34,22 @@ filter f (h ∷ hs) ≔ if (f h)
    (h ∷ filter f hs)
    (filter f hs);
 
-length : {A : Type} → List A → ℕ;
+length : {A : Type} → List A → Nat;
 length nil ≔ zero;
 length (_ ∷ l) ≔ suc (length l);
 
 reverse : {A : Type} → List A → List A;
 reverse ≔ foldl (flip (∷)) nil;
 
-replicate : {A : Type} → ℕ → A → List A;
+replicate : {A : Type} → Nat → A → List A;
 replicate zero _ ≔ nil;
 replicate (suc n) x ≔  x ∷ replicate n x;
 
-take : {A : Type} → ℕ → List A → List A;
+take : {A : Type} → Nat → List A → List A;
 take (suc n) (x ∷ xs) ≔ x ∷ take n xs;
 take _ _ ≔ nil;
 
-splitAt : {A : Type} → ℕ → List A → List A × List A;
+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;

Stdlib/Data/Maybe.juvix

@@ -6,11 +6,11 @@ inductive Maybe (A : Type) {
 };
 
 fromMaybe : {A : Type} → A → Maybe A → A;
-fromMaybe a nothing ≔ a;
-fromMaybe _ (just a) ≔ a;
+fromMaybe a nothing := a;
+fromMaybe _ (just a) := a;
 
 maybe : {A : Type} → {B : Type} → B → (A → B) → Maybe A → B;
-maybe b _ nothing ≔ b;
-maybe _ f (just a) ≔ f a;
+maybe b _ nothing := b;
+maybe _ f (just a) := f a;
 
 end;

Stdlib/Data/Nat.juvix

@@ -3,50 +3,50 @@ module Stdlib.Data.Nat;
 open import Stdlib.Data.String;
 
 builtin natural
-inductive ℕ  {
-  zero : ℕ;
-  suc : ℕ → ℕ;
+inductive Nat  {
+  zero : Nat;
+  suc : Nat → Nat;
 };
 
 infixl 6 +;
 builtin natural-plus
-+ : ℕ → ℕ → ℕ;
-+ zero b ≔ b;
-+ (suc a) b ≔ suc (a + b);
++ : Nat → Nat → Nat;
++ zero b := b;
++ (suc a) b := suc (a + b);
 
 infixl 7 *;
-* : ℕ → ℕ → ℕ;
-* zero b ≔ zero;
-* (suc a) b ≔ b + (a * b);
+* : Nat → Nat → Nat;
+* zero b := zero;
+* (suc a) b := b + (a * b);
 
-one : ℕ;
+one : Nat;
 one ≔ suc zero;
 
-two : ℕ;
+two : Nat;
 two ≔ suc one;
 
-three : ℕ;
+three : Nat;
 three ≔ suc two;
 
-four : ℕ;
+four : Nat;
 four ≔ suc three;
 
-five : ℕ;
+five : Nat;
 five ≔ suc four;
 
-six : ℕ;
+six : Nat;
 six ≔ suc five;
 
-seven : ℕ;
+seven : Nat;
 seven ≔ suc six;
 
-eight : ℕ;
+eight : Nat;
 eight ≔ suc seven;
 
-nine : ℕ;
+nine : Nat;
 nine ≔ suc eight;
 
-axiom natToStr : ℕ → String;
+axiom natToStr : Nat → String;
 compile natToStr {
   c ↦ "intToStr";
 };

Stdlib/Data/Nat/Ord.juvix

@@ -4,30 +4,30 @@ open import Stdlib.Data.Nat;
 open import Stdlib.Data.Ord;
 open import Stdlib.Data.Bool;
 
-compare : ℕ → ℕ → Ordering;
+compare : Nat → Nat → Ordering;
 compare zero zero ≔ EQ;
 compare zero _ ≔ LT;
 compare (suc _) zero ≔ GT;
-compare (suc a) (suc b) ≔ compare a b;
+compare (suc a) (suc b) := compare a b;
 
 infix 4 ==;
-== : ℕ → ℕ → Bool;
-== a b ≔ isEQ (compare a b);
+== : Nat → Nat → Bool;
+== a b := isEQ (compare a b);
 
 infix 4 <;
-< : ℕ → ℕ → Bool;
-< a b ≔ isLT (compare a b);
+< : Nat → Nat → Bool;
+< a b := isLT (compare a b);
 
 infix 4 <=;
-<= : ℕ → ℕ → Bool;
-<= a b ≔ not (isGT (compare a b));
+<= : Nat → Nat → Bool;
+<= a b := not (isGT (compare a b));
 
 infix 4 >;
-> : ℕ → ℕ → Bool;
-> a b ≔ isGT (compare a b);
+> : Nat → Nat → Bool;
+> a b := isGT (compare a b);
 
 infix 4 >=;
->= : ℕ → ℕ → Bool;
->= a b ≔ not (isLT (compare a b));
+>= : Nat → Nat → Bool;
+>= a b := not (isLT (compare a b));
 
 end;

Stdlib/Data/Product.juvix

@@ -7,24 +7,24 @@ inductive × (A : Type) (B : Type) {
 };
 
 uncurry : {A : Type} → {B : Type} → {C : Type} → (A → B → C) → A × B → C;
-uncurry f (a , b) ≔ f a b;
+uncurry f (a , b) := f a b;
 
 fst : {A : Type} → {B : Type} → A × B → A;
 fst (a , _) ≔ a;
 
 snd : {A : Type} → {B : Type} → A × B → B;
-snd (_ , b) ≔ b;
+snd (_ , b) := b;
 
 swap : {A : Type} → {B : Type} → A × B → B × A;
-swap (a , b) ≔ b , a;
+swap (a , b) := b , a;
 
 first : {A : Type} → {B : Type} → {A' : Type} → (A → A') → A × B → A' × B;
-first f (a , b) ≔ f a , b;
+first f (a , b) := f a , b;
 
 second : {A : Type} → {B : Type} → {B' : Type} → (B → B') → A × B → A × B';
-second f (a , b) ≔ a , f b;
+second f (a , b) := a , f b;
 
 both : {A : Type} → {B : Type} → (A → B) → A × A → B × B;
-both f (a , b) ≔ f a , f b;
+both f (a , b) := f a , f b;
 
 end;

Stdlib/Data/String/Ord.juvix

@@ -16,6 +16,6 @@ compile eqString  {
 
 infix 4 ==;
 == : String → String → Bool;
-== s1 s2 ≔ from-backend-bool (eqString s1 s2);
+== s1 s2 := from-backend-bool (eqString s1 s2);
 
 end;

Stdlib/Function.juvix

@@ -11,14 +11,14 @@ id : {A : Type} → 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;
+flip f b a := f a b;
 
 infixr 0 $;
 $ : {A : Type} → {B : Type} → (A → B) → A → B;
 $ f x ≔ f x;
 
 infixl 0 on;
 on : {A : Type} → {B : Type} → {C : Type} → (B -> B -> C) -> (A -> B) -> A -> A -> C;
-on f g a b ≔ f (g a) (g b);
+on f g a b := f (g a) (g b);
 
 end;

Stdlib/System/IO.juvix

@@ -7,7 +7,7 @@ builtin IO axiom IO : Type;
 
 infixl 1 >>;
 builtin IO-sequence axiom >> : IO → IO → IO;
-builtin natural-print axiom printNat : ℕ → IO;
+builtin natural-print axiom printNat : Nat → IO;
 
 axiom putStr : String → IO;
 compile putStr {