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: Dec 20 2023 at 11:08 UTC