How do I find out where notation is defined?

Stream: new members

[Kent Van Vels]

I constructing my toy version of the real numbers and I want to show that it has the least upper bound property. Do do so, a key step is to show that every set of real numbers that is bounded is bounded by an integer. This proof/function is (equivalent to) least_of_bdd that is defined in docs#int.least_of_bdd. It reads

def least_of_bdd {P : ℤ → Prop} [decidable_pred P]
  (b : ℤ) (Hb : ∀ z : ℤ, P z → b ≤ z) (Hinh : ∃ z : ℤ, P z) :
  {lb : ℤ // P lb ∧ (∀ z : ℤ, P z → lb ≤ z)} :=

That is my problem. My question is what does the double forward slash mean and how could I have found this information without bothering the Zulip chat? I use emacs and I am able to get the definition of functions by right-clicking, but I seemingly can't do this on notation.

Thank you.

[Kent Van Vels]

I just found out it is a docs@data.subtype notation. Sorry for the bother. I should just ask the rubber duck next to my desk.

[Kyle Miller]

No, that's perfectly fine to ask about // here. I remember it taking a while before I tracked down what it was. This one is built into Lean itself.

[Kyle Miller]

One trick you can do is use the set_option pp.notation false command, then maybe #print least_of_bdd.

[Ruben Van de Velde]

I wonder if we could have a page on the website with all the unsearchable basic notations

[Kyle Miller]

Another trick (which I suggest as an emacs user myself) is to pull up VS Code and use it's very handy widgets system. You can click on notations in the goal window and get more information.

[Jason Rute]

Here are a number of approaches, many already mentioned: https://proofassistants.stackexchange.com/questions/1672/in-lean-how-do-i-expand-a-definition-without-knowing-what-it-is/1673#1673