Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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?

view this post on Zulip Patrick Massot (Mar 08 2019 at 13:33):

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

view this post on Zulip Sebastian Ullrich (Mar 08 2019 at 14:36):

Yes. I definitely want that as well.

view this post on Zulip matt rice (Mar 08 2019 at 16:33):

the following seems to work

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

view this post on Zulip 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