## Stream: new members

### Topic: Deconstructing arguments

#### Brice Paris (Jan 22 2021 at 19:31):

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 (Jan 22 2021 at 19:36):

You can do

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


#### Brice Paris (Jan 22 2021 at 19:43):

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 (Jan 22 2021 at 19:57):

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

Last updated: Dec 20 2023 at 11:08 UTC