Subscripts don't work

[kevinsullivan]

Using an up-to-date Lean and VSCode lean install, I can get subscript characters such as m and x by using _m and _x, but it doesn't work for some other characters. For example _w leaves the w in normal font size and with an error message about an unexpected token.

[kevinsullivan]

Okay, apparently not all alphanumeric characters are supported as subscripts in the unicode definitions being used here: http://ftp.unicode.org/Public/UNIDATA/UnicodeData.txt.

I suggest adding the following sentence to the end of the first paragraph in Section 6.6 of TPiL, right after this sentence: "They can also include subscripts, which can be entered by typing _ followed by the desired subscripted character."

To add: "The Unicode character set that VSCode uses supports only the most commonly used characters as subscripts. These include, for example, m but not w. For more information on what characters can be used as subscripts, see http://ftp.unicode.org/Public/UNIDATA/UnicodeData.txt."

[bryangingechen]

This has also bitten me. I'd support your suggestion to improve TPiL; its repo can be found here. You might also find Ed Ayers's (draft?) doc on unicode in lean here helpful.