unicode subscripts and superscripts

Stream: general

[Alexander Bentkamp]

I find it mildly annoying that unicode does not have a complete set of latin superscripts and subscripts. Maybe it would be worth a try to propose to the unicode team to add them? A subscript f would clearly be more useful than a bubble tea emoji🧋, wouldn't it?

[Eric Wieser]

See also:

• https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/VSCode.3A.20lowercase.20letter.20subscript/near/243541877
• https://github.com/stevengj/subsuper-proposal

[Alexander Bentkamp]

Wow, the proposal (https://github.com/stevengj/subsuper-proposal) looks great! @Sarah Smith There are clearly more important things that Lean needs right now, but do you think it would be possible to get an endorsement from Microsoft for this proposal? That would definitely give it a big push.