Zulip Chat Archive

Stream: new members

Topic: meaning of ⦃


Heather Macbeth (Aug 28 2020 at 23:54):

What does mean? For example, in docs#upper_bounds . I am sure this has been asked and answered many times before, but unfortunately it's pretty hard to search Zulip for a single symbol ...

Scott Morrison (Aug 29 2020 at 00:05):

It is an implicit argument that Lean will not fill in with a metavariable (and hence presumably try to solve by unification), unless a subsequent explicit argument appears.

So:

def f {n:nat} := n
#check f --- just a `nat`, but that has a metavariable in it!
def g n:nat := n
#check g -- still a function

Heather Macbeth (Aug 29 2020 at 00:37):

Thank you! I have to say, I am still curious why would one want this ... if there is a good link in #tpil or a previous discussion, I would be glad of further reading :)

Bryan Gin-ge Chen (Aug 29 2020 at 00:39):

There's a brief discussion in TPiL here.

Heather Macbeth (Aug 29 2020 at 00:41):

That's perfect, thank you!

Johan Commelin (Aug 29 2020 at 04:06):

@Heather Macbeth It took me a long time to understand why these brackets are useful. But here is a very pedestrian reason:

  1. function.injective uses this in its statement: \forall \{{x y\}}, f x = f y -> x = y.
  2. We have things like function.injective.eq_iff, and we want to use projection notation like hf.eq_iff (for some hf : function.injective f).
  3. If we had used \forall {x y} then lean would try to figure out x and y whenever it saw hf, and so hf would not have type function.injective f anymore, and projection notation would break down. The other option would be to use (x y).
  4. Suppose that h : f x = f y. Then hf h will be a proof of x = y. This still just works. But if we used \forall (x y), then we would have to write explicitly hf x y h, which seems a bit annoying.

Tl;dr: \{{ .. \}} hold a charming spot between {} and ().

Heather Macbeth (Aug 29 2020 at 04:09):

This is great! Thanks @Johan Commelin


Last updated: Dec 20 2023 at 11:08 UTC