Zulip Chat Archive

Stream: general

Topic: unicode subscripts and superscripts


Alexander Bentkamp (Jul 27 2022 at 12:25):

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 (Jul 27 2022 at 12:52):

See also:

Alexander Bentkamp (Jul 27 2022 at 13:40):

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.


Last updated: Aug 03 2023 at 10:10 UTC