Zulip Chat Archive
Stream: PR reviews
Topic: leanprover/vscode-lean#170 Add missing Unicode subscripts...
Utensil Song (Jun 16 2020 at 05:55):
A minor PR leanprover/vscode-lean#170 : Add missing Unicode subscripts and superscripts .
(Possibly this doesn't need a topic here, but opened it for any potential discussion anyway)
Last updated: Dec 20 2023 at 11:08 UTC