RFC: Unicode alternative `≔` for `:=` in definitions

Stream: lean4

[Anqur]

For the colon equal symbol (:=), could we have a unicode version of it in the definition syntax? I.e. ≔.

Full example:

def n ≔ 42

[Patrick Massot]

I love unicode in general, but here I struggle to see what would be gain. Could you expand a bit on your motivation?

[Patrick Massot]

And let me check: do you know about fonts with ligatures?

[Anqur]

Yes I know the ligatures, I use them often with Fira Code.

The parser itself already has many "unicode alternatives", e.g.

1. Arrow (depArrow): → and ->
2. Forall: ∀ and forall
3. Another arrow (basicFun): ↦ and =>
4. Lambda: λ and fun

So I believe it's okay (and even better) to keep/expand this convention, or, consistency, since initially I felt a bit surprised that many unicode symbols are supported, but the colon equal gets its name in the unicode table, having no its presence in the syntax.

[Patrick Massot]

But the unicode version is basically indistinguishable from the ascii version, especially with ligatures. This is very different from the other examples you give.

[Julian Berman]

(See also previously https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/A.20plea.20from.20a.20newbie.20concerning.20future.20Unicode.20use though IMHO that thread hugely conflates two separate issues of "do we need ASCII equivalents for all unicode symbols" with "is it OK to use highly confusable versions of the same symbol for very different things, regardless of whether that symbol is ASCII or unicode" -- but it does contain some opinions from Mario and others on adding more ASCII equivalents.)

[Anqur]

@Patrick Massot Cool and thanks for pointing out its indistinguishable look and further issues.

Ligature is something in an editor/IDE, but not generally the web. Unicode symbols will stand out for having the following advantages:

• Single and monospaced character that fits rest of the code (although sometimes it doesn't)
• More literate on web with web-safe fonts (for being shorter, monospaced, mostly available everywhere)

But I'm not here standing for/against some ASCII-ism vs Unicode-ism, I just arrived looking for some consistent and coherent convention of Unicode in Lean 4.

A further context is, I was writing a book that introduces the implementation of a theorem prover, and Lean 4 syntax is my go. My intuition told me that a ≔ in the definition syntax should be valid but oops it's not.

@Julian Berman Thanks for mentioning this discussion. I'm afraid the "two issues" (universal ASCII alternatives and confusable Unicode symbols) go out of the scope here. However, it's good to see similar topics being discussed, and I love the "ship has sailed" phrase, and it kinda fits here.

[Jon Eugster]

as for some history on how unicode is added/removed in core Lean syntax, I think (3.) above got added because many people doing mathematics wished for it and it does not only look nicer, it can also help distinguish the different meanings => can have in Lean (e.g. match). And I believe there are/were wishes to remove (4.) because it blocks the symbol from being used as local variable/name.

I don't think there is an inherit reason Lean couldn't use the unicode :=, but unless reasonable evidence exists that anybody would benefit from it, I doubt any core developer would be motivated to implement it (and add it to things that need to be maintained). I have a hunch that since it's part of various syntax it's more evolved than just defining a new notation, but I didnt really think about these details:thinking:

[Kevin Buzzard]

Oh yeah I guess := means several different things, and it's kind of a bit confusing that currently we are in a situation where => can be replaced by \mapsto sometimes but not always (for the same reason). This proposal would probably mean more of that.