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: May 02 2025 at 03:31 UTC