Search for notation

Stream: new members

[María Inés de Frutos Fernández]

Where is the notation ∀ᶠ introduced? More generally, is there a good way to search for notation in the documentation?

[Alex J. Best]

It is just after src#filter.eventually

[María Inés de Frutos Fernández]

Thanks, Alex!

[Riccardo Brasca]

In VS Code if you with the cursor over that symbol, it says "filter.eventually...".

[Alex J. Best]

I don't think the doc is too easy to search, I would either right click the notation and click go to definition or search for notation.*∀ᶠ in the vscode search with "use regular expressions" turned on.

[Riccardo Brasca]

The problem with right click a notation is that often (not in this case I think) it sends you to has_notation that is rarely useful, if you want to know, for example, what M ≤ N means when M and N modules.

[Johan Commelin]

Can we have notation#∀ᶠ be a link?

[Johan Commelin]

And can the docs list all the notation and localized "notation occurences in mahtlib?

[María Inés de Frutos Fernández]

Alex J. Best said:

I don't think the doc is too easy to search, I would either right click the notation and click go to definition or search for notation.*∀ᶠ in the vscode search with "use regular expressions" turned on.

I tried right click, but it told me "no definition found for ∀ᶠ".

[Riccardo Brasca]

Wait for the orange bar to be gone.

[María Inés de Frutos Fernández]

I'm not getting an orange bar.

[Bryan Gin-ge Chen]

Johan Commelin said:

And can the docs list all the notation and localized "notation occurences in mahtlib?

doc-gen#94 is related. We'll need that or something like it before we can get notation# to work.

[Johan Commelin]

Aah, thanks for the pointer.

[Johan Commelin]

But do we need to do this using Lean? I guess we could also just grep for these commands, and format the list with a bit of html.

[Johan Commelin]

Wouldn't that be good enough?

[Alex J. Best]

Huh that's weird, right clicking did work for me, though I do find it to be flakey sometimes. I tried to right click it from #check ∀ᶠ, does that make any difference?

[Bryan Gin-ge Chen]

Johan Commelin said:

Wouldn't that be good enough?

It might be! (As far as doc-gen goes I think I'm still supposed to be looking into collecting all the stacks tags in one place...)

[María Inés de Frutos Fernández]

Alex J. Best said:

Huh that's weird, right clicking did work for me, though I do find it to be flakey sometimes. I tried to right click it from #check ∀ᶠ, does that make any difference?

It's now working for me too (I don't know why it wasn't before ). Searching with regular expressions did work at the first try, thanks!

[Johan Commelin]

(@Bryan Gin-ge Chen I think there were plans to collect the stacks tags using an attribute? But it hasn't been high prio recently.)

[Eric Wieser]

Why do we need that linked issue before we can make notation# work? Don't we just open every locale right now?

[Kevin Buzzard]

Johan Commelin said:

Can we have notation#∀ᶠ be a link?

@Shing Tak Lam your bot on the discord server does this, right?

[Yaël Dillies]

with the command icode :grinning_face_with_smiling_eyes:

[Shing Tak Lam]

Kevin Buzzard said:

Johan Commelin said:

Can we have notation#∀ᶠ be a link?

Shing Tak Lam your bot on the discord server does this, right?

image.png

[Kevin Buzzard]

Oh so it only tells you how to type it, not how to find it.

[Shing Tak Lam]

Yeah, it basically takes the VSCode replacements file and does a search on that. It doesn't tell you what the notation is actually for.