Deconstructing arguments

Stream: new members

[Brice Paris]

New to Lean, working through theorem_proving_in_lean.

My solution for uncurry exercise on the dependent type theory section ends up as
def uncurry (α β γ : Type*) (f: α → β → γ ) : α × β → γ := λ c, f c.fst c.snd

Is there a more general way I can access the fst and snd components of the product in the lambda?

Why doesnt something like
def uncurry2 (α β γ : Type*) (f: α → β → γ ) : α × β → γ := λ (a × b), f a b work ?

[Alex J. Best]

You can do

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

[Brice Paris]

The angle brackets are another way to represent a prod term ? Then why do(a \x \b) or (prod a b) not decompose ?

[Yakov Pechersky]

prod α β or α × β : Type* is a term describing a Type, while (a, b) or ⟨a, b⟩ : α × β is a term of that product type.