Remove usages of ≔ and replace those with :=

[jonaprieto]

(originally by @james-chf)

the difference between ≔ and = is hard to spot, I thought = was the symbol to use when writing function clauses

[jonaprieto]

We decided to remove all the Unicode input from the examples and the standard without removing support for typing them.

[lukaszcz]

They unicode ≔ is still present in the examples.

[lukaszcz]

In fact, I would advocate removing ≔ and the unicode cons ∷ entirely. I don't see the point of having a unicode symbol which is supposed to look exactly like a combination of two ASCII characters. What is gained here except for confusion?

With lambda, forall, etc, even arrow, one can argue that unicode is more concise and corresponds more closely to the mathematical symbols one really wants to represent, which makes the text more readable (though not necessarily writable without substantial IDE support). Those symbols can't be represented faithfully with ASCII characters. But ≔ and ∷ ? They are supposed to look exactly or almost exactly like := and ::, so what's the point?

The ≔ is even worse than ∷ in this respect, because with many fonts it actually looks almost like "=" not ":=", which only adds to the confusion.

[lukaszcz]

BTW, the removal (anoma/juvix-stdlib#15) was very incomplete:

https://github.com/anoma/juvix-stdlib/blob/main/Stdlib/Data/List/Ord.juvix
https://github.com/anoma/juvix-stdlib/blob/main/Stdlib/Data/List.juvix
https://github.com/anoma/juvix-stdlib/blob/main/Stdlib/Data/Bool.juvix
https://github.com/anoma/juvix-stdlib/blob/main/Stdlib/Data/Nat/Ord.juvix

[lukaszcz]

Btw, I like the way Lean introduces unicode, how unicode is used, and the general feel of the syntax:

https://leanprover.github.io/theorem_proving_in_lean4/dependent_type_theory.html#simple-type-theory