Lean also makes heavy use of non-ascii characters (inserted into texts using a LaTeX-inspired backslash-and-then-name , in a number of editors). It also has wa

Lean also makes heavy use of non-ascii characters (inserted into texts using a LaTeX-inspired backslash-and-then-name , in a number of editors). It also has ways to write the same things in ascii, but it is a fair bit less convenient to read.