'⟨' and '⟩' in binder of lambda abstraction

Stream: new members

[Gun Pinyo]

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]

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

[Sebastian Ullrich]

Yes. I definitely want that as well.

[matt rice]

the following seems to work

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

[Mario Carneiro]

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