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?

  • 5
    $\begingroup$ I understand the urge to use ASCII (heck, I think libraries should store paper) – but could you explain what your worry is about? Is it about the human-computer interaction, i.e., that the human will be confused? Or that we won't be able to backport Lean to 1970 when we invent time travel? The HCI worry is real: the other day a colleague complained Agda standard library used Unicode whitespaces as operators (he was using a font with missing Unicode characters). If we invent time travel, Unicode won't be the main problem. $\endgroup$ Mar 4, 2022 at 6:47
  • 2
    $\begingroup$ more interesting question might be to know the list of Unicode chars that Lean reserved for operators etc., e.g. $\lambda$ $\endgroup$ Mar 4, 2022 at 9:29
  • 2
    $\begingroup$ @GuyCoder: You're getting younger. $\endgroup$ Mar 4, 2022 at 13:09

2 Answers 2


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)).


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.

  • 2
    $\begingroup$ (You might reasonably point a finger at me, for introducing the arrow used in the category theory library as an alternative to the usual function arrow built in to the language.) $\endgroup$ Mar 6, 2022 at 5:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.