remove ≔ from the language and replace it by := (#1563)

* remove ≔ from the language and replace it by :=

* revert accidental changes in juvix input mode

* update stdlib submodule

* rename ℕ by Nat in the tests and examples

* fix shell tests

README.org

@@ -126,7 +126,7 @@ module HelloWorld;
 open import Stdlib.Prelude;
 
 main : IO;
-main ≔ putStrLn "hello world!";
+main := putStrLn "hello world!";
 
 end;
 #+end_src

docs/org/examples/backend-specific/minic-hello-world.org

@@ -25,7 +25,7 @@ compile put-str-ln {
 };
 
 main : Action;
-main ≔ put-str-ln "hello world!";
+main := put-str-ln "hello world!";
 
 end;
 #+end_src

docs/org/examples/validity-predicates/PolyFungibleToken.org

@@ -19,17 +19,17 @@ inductive Bool {
 
 infixr 2 ||;
 || : Bool → Bool → Bool;
-|| false a ≔ a;
-|| true _ ≔ true;
+|| false a := a;
+|| true _ := true;
 
 infixr 3 &&;
 && : 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 false _ b ≔ b;
+if true a _ := a;
+if false _ b := b;
 
 --------------------------------------------------------------------------------
 -- Backend Booleans
@@ -67,14 +67,14 @@ compile bool {
 };
 
 from-backend-bool : BackendBool → Bool;
-from-backend-bool bb ≔ bool bb true false;
+from-backend-bool bb := bool bb true false;
 
 --------------------------------------------------------------------------------
 -- Functions
 --------------------------------------------------------------------------------
 
 id : {A : Type} → A → A;
-id a ≔ a;
+id a := a;
 
 --------------------------------------------------------------------------------
 -- Integers
@@ -93,7 +93,7 @@ compile <' {
 
 infix 4 <;
 < : Int → Int → Bool;
-< i1 i2 ≔ from-backend-bool (i1 <' i2);
+< i1 i2 := from-backend-bool (i1 <' i2);
 
 axiom eqInt : Int → Int → BackendBool;
 compile eqInt {
@@ -102,7 +102,7 @@ compile eqInt {
 
 infix 4 ==Int;
 ==Int : Int → Int → Bool;
-==Int i1 i2 ≔ from-backend-bool (eqInt i1 i2);
+==Int i1 i2 := from-backend-bool (eqInt i1 i2);
 
 infixl 6 -;
 axiom - : Int -> Int -> Int;
@@ -132,7 +132,7 @@ compile eqString  {
 
 infix 4 ==String;
 ==String : String → String → Bool;
-==String s1 s2 ≔ from-backend-bool (eqString s1 s2);
+==String s1 s2 := from-backend-bool (eqString s1 s2);
 
 --------------------------------------------------------------------------------
 -- Lists
@@ -145,12 +145,12 @@ 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;
 
 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;
 
 --------------------------------------------------------------------------------
 -- Pair
@@ -172,17 +172,17 @@ inductive Maybe (A : Type) {
 };
 
 from-int : Int → Maybe Int;
-from-int i ≔ if (i < 0) nothing (just i);
+from-int i := if (i < 0) nothing (just i);
 
 maybe : {A : Type} → {B : Type} → B → (A → B) → Maybe A → B;
-maybe b _ nothing ≔ b;
-maybe _ f (just x) ≔ f x;
+maybe b _ nothing := b;
+maybe _ f (just x) := f x;
 
 from-string : String → Maybe String;
-from-string s ≔ if (s ==String "") nothing (just s);
+from-string s := if (s ==String "") nothing (just s);
 
 pair-from-optionString : (String → Int × Bool) → Maybe String → Int × Bool;
-pair-from-optionString ≔ maybe (0 , false);
+pair-from-optionString := maybe (0 , false);
 
 --------------------------------------------------------------------------------
 -- Anoma
@@ -204,44 +204,44 @@ compile isBalanceKey {
 };
 
 read-pre : String → Maybe Int;
-read-pre s ≔ from-int (readPre s);
+read-pre s := from-int (readPre s);
 
 read-post : String → Maybe Int;
-read-post s ≔ from-int (readPost s);
+read-post s := from-int (readPost s);
 
 is-balance-key : String → String → Maybe String;
-is-balance-key token key ≔ from-string (isBalanceKey token key);
+is-balance-key token key := from-string (isBalanceKey token key);
 
 unwrap-default : Maybe Int → Int;
-unwrap-default ≔ maybe 0 id;
+unwrap-default := maybe 0 id;
 
 --------------------------------------------------------------------------------
 -- Validity Predicate
 --------------------------------------------------------------------------------
 
 change-from-key : String → Int;
-change-from-key key ≔ unwrap-default (read-post key) - unwrap-default (read-pre key);
+change-from-key key := unwrap-default (read-post key) - unwrap-default (read-pre key);
 
 check-vp : List String → String → Int → String → Int × Bool;
-check-vp verifiers key change owner ≔
+check-vp verifiers key change owner :=
     if
         (change-from-key key < 0)
         -- make sure the spender approved the transaction
         (change + (change-from-key key), elem (==String) owner verifiers)
         (change + (change-from-key key),  true);
 
 check-keys : String → List String → Int × Bool → String → Int × Bool;
-check-keys token verifiers (change , is-success) key ≔
+check-keys token verifiers (change , is-success) key :=
     if
         is-success
         (pair-from-optionString (check-vp verifiers key change) (is-balance-key token key))
         (0 , false);
 
 check-result : Int × Bool → Bool;
-check-result (change , all-checked) ≔ (change ==Int 0) && all-checked;
+check-result (change , all-checked) := (change ==Int 0) && all-checked;
 
 vp : String → List String → List String → Bool;
-vp token keys-changed verifiers ≔
+vp token keys-changed verifiers :=
     check-result
         (foldl
             (check-keys token verifiers)
@@ -274,33 +274,33 @@ compile >> {
 };
 
 show-result : Bool → String;
-show-result true ≔ "OK";
-show-result false ≔ "FAIL";
+show-result true := "OK";
+show-result false := "FAIL";
 
 --------------------------------------------------------------------------------
 -- Testing VP
 --------------------------------------------------------------------------------
 
 token : String;
-token ≔ "owner-token";
+token := "owner-token";
 
 owner-address : String;
-owner-address ≔ "owner-address";
+owner-address := "owner-address";
 
 change1-key : String;
-change1-key ≔ "change1-key";
+change1-key := "change1-key";
 
 change2-key : String;
-change2-key ≔ "change2-key";
+change2-key := "change2-key";
 
 verifiers : List String;
-verifiers ≔ owner-address ∷ nil;
+verifiers := owner-address ∷ nil;
 
 keys-changed : List String;
-keys-changed ≔ change1-key ∷ change2-key ∷ nil;
+keys-changed := change1-key ∷ change2-key ∷ nil;
 
 main : Action;
-main ≔
+main :=
     (putStr "VP Status: ")
     >> (putStrLn (show-result (vp token keys-changed verifiers)));
 

docs/org/language-reference/builtins.org

@@ -19,8 +19,8 @@ Juvix has support for the built-in natural type and a few functions that are com
    inifl 6 +;
    builtin natural-plus
    + : Nat → Nat → Nat;
-   + zero b ≔ b;
-   + (suc a) b ≔ suc (a + b);
+   + zero b := b;
+   + (suc a) b := suc (a + b);
    #+end_example
 
 3. Builtin axiom definitions.

docs/org/language-reference/foreign-blocks.org

@@ -32,5 +32,5 @@ compile <' {
 
 infix 4 <;
 < : Int → Int → Bool;
-< a b ≔ from-backend-bool (a <' b);
+< a b := from-backend-bool (a <' b);
 #+end_example

docs/org/language-reference/functions.org

@@ -42,9 +42,9 @@ odd : Nat → Bool;
 
 even : Nat → Bool;
 
-odd zero ≔ false;
-odd (suc n) ≔ even n;
+odd zero := false;
+odd (suc n) := even n;
 
-even zero ≔ true;
-even (suc n) ≔ odd n;
+even zero := true;
+even (suc n) := odd n;
 #+end_example

docs/org/language-reference/inductive-data-types.org

@@ -30,8 +30,8 @@ Let us define, for example, the function for adding two natural numbers.
 #+begin_src text
 inifl 6 +;
 + : Nat → Nat → Nat;
-+ zero b ≔ b;
-+ (suc a) b ≔ suc (a + b);
++ zero b := b;
++ (suc a) b := suc (a + b);
 #+end_src
 
 As mentioned earlier, an inductive type may have type parameters. The canonical
@@ -49,8 +49,8 @@ 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;
 #+end_example
 
 To see more examples of inductive types and how to use them, please check out

docs/org/notes/builtins.org

@@ -22,8 +22,8 @@ of definitions:
    inifl 6 +;
    builtin natural-plus
    + : Nat → Nat → Nat;
-   + zero b ≔ b;
-   + (suc a) b ≔ suc (a + b);
+   + zero b := b;
+   + (suc a) b := suc (a + b);
    #+end_src
 
 3. Builtin axiom definitions. For example:

docs/org/notes/monomorphization.org

@@ -10,22 +10,22 @@
  Example:
  #+begin_src juvix
  id : (A : Type) → A → A;
- id _ a ≔ a;
+ id _ a := a;
 
  b : Bool;
- b ≔ id Bool true;
+ b := id Bool true;
 
  n : Nat;
- n ≔ id Nat zero;
+ n := id Nat zero;
  #+end_src
 
  Is translated into:
  #+begin_src juvix
  id_Bool : Bool → Bool;
- id_Bool a ≔ a;
+ id_Bool a := a;
 
  id_Nat : Nat → Nat;
- id_Nat a ≔ a;
+ id_Nat a := a;
  #+end_src
 
 * More examples
@@ -37,14 +37,14 @@ inductive List (A : Type) {
 };
 
 even : (A : Type) → List A → Bool;
-even A nil ≔ true ;
-even A (cons _ xs) ≔ not (odd A xs) ;
+even A nil := true ;
+even A (cons _ xs) := not (odd A xs) ;
 
 odd : (A : Type) → List A → Bool;
-odd A nil ≔ false ;
-odd A (cons _ xs) ≔ not (even A xs) ;
+odd A nil := false ;
+odd A (cons _ xs) := not (even A xs) ;
 
--- main ≔ even Bool ..  odd Nat;
+-- main := even Bool ..  odd Nat;
 #+end_src
 
 * Collection algorithm
@@ -158,7 +158,7 @@ list of concrete type applications involving =f=: =f â₁, …, f âₙ=.
  be the variables bound in =pₘ₊₁, …, pₖ=. Let =w'₁, …, w'ₛ= be fresh variables.
  Then let =δ = {w₁ ↦ w'₁, …, wₛ ↦ w'ₛ}=.
 
- Now let =𝒞'= have patterns =δ(pₘ₊₁), …, δ(pₖ)= and let =e' ≔ (σ ∪ δ)(e)=. It
+ Now let =𝒞'= have patterns =δ(pₘ₊₁), …, δ(pₖ)= and let =e' := (σ ∪ δ)(e)=. It
  should be clear that =e'= has no type variables in it and that all local
  variable references in =e'= are among =w'₁, …, w'ₛ=. Note that =e'= is not yet
  monomorphized. Proceed to the next step to achieve that.
@@ -172,7 +172,7 @@ list of concrete type applications involving =f=: =f â₁, …, f âₙ=.
  view of the application: =f a₁ … aₘ=. Then, if =f= is either a constructor, or
  a function, let =A₁, …, Aₖ= with =k ≤ m= be the list of type parameters of =f=.
  - If =f= is a function and =f a₁ … aₖ ∉ ℒ= then recurse normally, otherwise,
-   let =â ≔ a₁ … aₖ= and replace the original expression =f a₁ … aₘ=, by =⋆(f â)
+   let =â := a₁ … aₖ= and replace the original expression =f a₁ … aₘ=, by =⋆(f â)
    aₖ₊₁' … aₘ'= where =aₖ₊₁' … aₘ'= are the monomorphization of =aₖ₊₁ … aₘ=
    respectively.
  - If =f= is a constructor, let =d= be its inductive type. Then check =d a₁ … aₖ

docs/org/tutorials/nodejs-interop.org

@@ -27,7 +27,7 @@ open import Stdlib.Prelude;
 axiom hostDisplayString : String → IO;
 
 juvixRender : IO;
-juvixRender ≔ hostDisplayString "Hello World from Juvix!";
+juvixRender := hostDisplayString "Hello World from Juvix!";
 
 end;
 #+end_src