## 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