Zulip Chat Archive
Stream: new members
Topic: input
Alex Zhang (Aug 11 2021 at 22:52):
Is it possible to write 1 similar to
image.png
in lean?
Kevin Buzzard (Aug 11 2021 at 22:54):
\b1
Eric Wieser (Aug 11 2021 at 22:54):
Kevin Buzzard (Aug 11 2021 at 22:57):
then paste into VS Code and hover over it for the shortcut
Last updated: Dec 20 2023 at 11:08 UTC