Stream: new members
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