## Stream: new members

### Topic: '⟨' and '⟩' in binder of lambda abstraction

#### Gun Pinyo (Mar 08 2019 at 13:25):

Hello, I have a question. Lean allows us to write '⟨' and '⟩' in a binder of lambda abstraction (as in uncurry1) but it will become an error as soon as I put a type annotation in the binder (as in uncurry2). It is weird since the type annotation works fine if there is no '⟨' and '⟩' in a binder of lambda abstraction (as in uncurry3).

  variable f : α → β → γ
def uncurry1 : α × β → γ := λ ⟨a, b⟩, f a b
def uncurry2 : α × β → γ := λ ⟨a, b⟩ : α × β, f a b
def uncurry3 : α × β → γ := λ p : α × β, f p.1 p.2


Is "not able to write a type annotation for '⟨' and '⟩'" a bug or intended feature?

#### Patrick Massot (Mar 08 2019 at 13:33):

I would say it's an absence of feature. @Sebastian Ullrich?

#### Sebastian Ullrich (Mar 08 2019 at 14:36):

Yes. I definitely want that as well.

#### matt rice (Mar 08 2019 at 16:33):

the following seems to work

  def uncurry4 : α × β → γ := λ ⟨(a : α), (b : β)⟩, f a b


#### Mario Carneiro (Mar 08 2019 at 18:07):

huh, this is news to me. It also works in pattern let

Last updated: May 15 2021 at 02:11 UTC