Looking up notation

Stream: new members

[Ben Lee]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

(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)

[Ben Lee]

Thanks!

I think I'm too new to answer the question about discord!

[Kevin Buzzard]

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]

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]

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

[Mario Carneiro]

I don't think it does anything

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

(and also for me!)

[Mario Carneiro]

we need a cheat sheet for reading notation commands as well

[Mario Carneiro]

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]

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