Lean File locations for notations

Stream: new members

[Garrison Venn]

I'm using VSCode and am not able to find the file that defines:

notation "⟦" t "⟧" => Quot.mk _ t

According to AI (which I'm trying to verify) this notation is standard, but I'm having to define it myself. I'm not using matlib, as I'm just playing with the basics of Quotient. It is not in Prelude.lean.

[Etienne Marion]

It's here: Quotient.«term⟦_⟧» (so in mathlib)

[Etienne Marion]

(Found it by looking for "⟦" in the documentation search bar)

[Garrison Venn]

Thanks. Can you explain how to do this? I used:

(Ctrl+Shift+P or Cmd+Shift+P)

and found:

Abbreviation
\[[]]
Unicode symbol
⟦$CURSOR⟧

but I don't know how to tie it back to the file it is "defined" in. Sorry VSCode is not my standard development editor (Emacs with Viper). It just seems simpler to learn Lean, and the VI extension makes it easy for me.

[Etienne Marion]

Typing \[[ should do it.

[Garrison Venn]

Unfortunately this may work if I imported Mathlib, maybe. Regardless without it, the Info View does not show anything relevant. I took your hint and used LeanExplore WEB interface and searched for:

\<<term\[[_\]]\>>

So I'm on my way to solving this for any notation. Just need to learn how to better use LeanExplore. Thanks for the help.

[Garrison Venn]

Cool using the Lean doc search for ⟦_⟧ worked. This is what you were referring to. Thanks again.

[Etienne Marion]

Of course as I said the notation is defined in Mathlib so if you don’t use Mathlib it won’t work.