Zulip Chat Archive

Stream: new members

Topic: How do I find out where notation is defined?


Kent Van Vels (Sep 23 2022 at 16:03):

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 (Sep 23 2022 at 16:11):

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 (Sep 23 2022 at 17:35):

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 (Sep 23 2022 at 17:35):

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

Ruben Van de Velde (Sep 23 2022 at 17:37):

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

Kyle Miller (Sep 23 2022 at 17:37):

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 (Sep 23 2022 at 19:51):

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


Last updated: Dec 20 2023 at 11:08 UTC