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
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
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
\r is the standard way?