Does Lean have a standard ASCII representation?

Question

From Lean 4 tutorial, I learned that

In the Lean standard library, you often see Greek letters to denote types, and the Unicode symbol → as a more compact version of ->

and you can also type the arrow symbol → as either \to or \r.

The use of Unicode worries me a little bit just as when I first saw the different zeros and ones (in bold font etc.) in Isabelle. I was worried that I might miss the fine differences between some Unicode symbols and ASCII, and maybe elsewhere given the very large alphabet of Unicode and the fact that I haven't seen all the Unicode characters. But I was relieved to see that the Isabelle thm files are/can be stored in pure ASCII forms such as

\<leftarrow>, \<one>, etc.

My questions are:

Does Lean have similar ASCII representations in Lean files? Or are Lean files inherently Unicode?

Are there canonical ASCII representations? e.g. which of ->, \to or \r is the standard way?

Answer 1

There is no standard ASCII representation that is equivalent to an arbitrary Lean 4 file using Unicode, and I'm not aware of such a thing for any other language. (Isabelle uses that encoding because it does not use Unicode and in fact adds many symbols and formatting not part of Unicode. Which makes looking at Isabelle files with any other tools, e.g. git, problematic).

The core term syntax accepts both ASCII and Unicode keywords:

src/Lean/Parser/Term.lean:@[builtinTermParser] def depArrow := leading_parser:25 bracketedBinder true >> unicodeSymbol " → " " -> " >> termParser
src/Lean/Parser/Term.lean:def «forall» := leading_parser:leadPrec unicodeSymbol "∀" "forall" >> many1 (ppSpace >> (simpleBinder <|> bracketedBinder)) >> ", " >> termParser
src/Lean/Parser/Term.lean:@[builtinTermParser] def «fun» := leading_parser:maxPrec ppAllowUngrouped >> unicodeSymbol "λ" "fun" >> (basicFun <|> matchAlts)

Many notations on top of this core, e.g. in Notation.lean, however, do not. The Lean standard library always prefers the Unicode variant except for fun (because working with Lean should be fun (this is not an officially endorsed statement)).

Answer 2

Answering specifically the concern:

I might miss the fine differences between some Unicode symbols

it may be worth noting that on hovering over a character in a Lean aware editor (e.g. the Lean extension to VSCode) shows a tooltip containing the \something code one can type to produce that character. (I guess some unicode characters used in Lean don't have such a code; if you notice these it's probably worth adding them!)

This can be used to disambiguate similar characters.

Further, it would be reasonable to object during a pull request, or to make a pull request, if there are files which are using unreasonably similar unicode symbols unnecessarily.