Stream: new members

Topic: Looking up notation

Ben Lee (Dec 20 2020 at 19:59):

Is this the best place to ask very basic questions? (or is Discord a better place to ask?)

I'm trying to understand some notation, what is the best way to look up notation? Specifically, what does the special brace in the definition of "is_compact" mean?
def is_compact (s : set α) := ∀ ⦃f⦄ [ne_bot f], f ≤ 𝓟 s → ∃a∈s, cluster_pt a f
the thing around the f.

Mario Carneiro (Dec 20 2020 at 20:01):

That is "semi-implicit", which means that it is automatically inserted only if you provide an argument after it

Mario Carneiro (Dec 20 2020 at 20:01):

That way you can write just h : is_compact s and it won't get auto-instantiated to h _

Mario Carneiro (Dec 20 2020 at 20:02):

but if you write h (h' : f <= P s) then that becomes h _ _ h' where the two arguments in between are inferred

Mario Carneiro (Dec 20 2020 at 20:03):

(Is discord starting to accumulate this much momentum? I may have to watch it more closely, although it's got a lot of noise on it)

Thanks!

Kevin Buzzard (Dec 20 2020 at 20:06):

Discord gets people involved but it's (intentionally) very noisy. I tend to tell people that they can feel free to chat/post memes on the Discord but serious lean questions like the above are more likely to be answered quickly on the Zulip

Mario Carneiro (Dec 20 2020 at 20:22):

Regarding the meta-question about notation, there is a way to look up notation using #print notation but it won't work in this case because this binder is part of the core syntax, there is no notation command that declares it

Kevin Buzzard (Dec 20 2020 at 20:24):

Certain pieces of notation are hard for beginners to find; maybe we should make a cheat sheet. What does #notation do?

Mario Carneiro (Dec 20 2020 at 20:25):

I don't think it does anything

Kevin Buzzard (Dec 20 2020 at 20:25):

Nothing :-) So does that mean there can be a website where notation not covered by #print notation can be documented?

Mario Carneiro (Dec 20 2020 at 20:26):

I guess we could just document all the keywords and tokens?

Kevin Buzzard (Dec 20 2020 at 20:26):

The notation which just leads you to scoped: r stuff is also hard for beginners to penetrate

Kevin Buzzard (Dec 20 2020 at 20:26):

(and also for me!)

Mario Carneiro (Dec 20 2020 at 20:27):

we need a cheat sheet for reading notation commands as well

Mario Carneiro (Dec 20 2020 at 20:28):

I looked it up once (I had to read the source), but it is indeed quite arcane and dissimilar to other lean expressions in a number of ways (like who thought that it would be a good idea to have a binder written (x y, p[x,y])?)

Bryan Gin-ge Chen (Dec 20 2020 at 20:28):

There's a related issue here and a few other documentation requests in the other issues.

Last updated: May 15 2021 at 23:13 UTC