Zulip Chat Archive
Stream: general
Topic: notation cheat sheet
Bernd Losert (Dec 06 2021 at 09:57):
Does anyone know of a notation cheat sheet? In particular, one with the ascii equivalents?
Huỳnh Trần Khanh (Dec 06 2021 at 10:02):
Huỳnh Trần Khanh (Dec 06 2021 at 10:03):
is this what you're looking for?
Bernd Losert (Dec 06 2021 at 10:09):
Almost. That lacks the ascii equivalents.
Bolton Bailey (Dec 06 2021 at 10:10):
The naming conventions page? https://leanprover-community.github.io/contribute/naming.html
Bernd Losert (Dec 06 2021 at 10:23):
Nice. The "Names of symbols" part is exactly what I need. Seems incomplete though.
Yaël Dillies (Dec 06 2021 at 10:36):
Yeah, there are many new things all the time, so it's hard to keep up to date.
Bernd Losert (Dec 06 2021 at 11:21):
Are the angle brackets ⟨⟩ defined as notation or is that built into the lean type checker?
Eric Wieser (Dec 06 2021 at 11:30):
That's builtin notation
Eric Wieser (Dec 06 2021 at 11:30):
Usually for mk, but it's possible to change the name of what they correspond to (eg ulift.up instead of ulift.mk, see src#ulift)
Bernd Losert (Dec 06 2021 at 11:38):
Aha. Thanks.
Mario Carneiro (Dec 06 2021 at 12:41):
The ascii equivalent for ⟨ is (|, but that is used exactly 0 times in mathlib, and the idea that everything has an ascii equivalent is soft-deprecated in mathlib so many new things won't have any ascii equivalents
Mario Carneiro (Dec 06 2021 at 12:41):
or rather, it was; it looks like it was removed in lean#265
Mario Carneiro (Dec 06 2021 at 12:43):
@Bernd Losert
Bernd Losert (Dec 06 2021 at 12:48):
Good to know. Thanks.
Last updated: Dec 20 2023 at 11:08 UTC