meaning of ⦃

Stream: new members

[Heather Macbeth]

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]

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]

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]

There's a brief discussion in TPiL here.

[Heather Macbeth]

That's perfect, thank you!

[Johan Commelin]

@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]

This is great! Thanks @Johan Commelin