## Stream: new members

### Topic: Curry/Uncurry

#### me myself and I (Sep 16 2019 at 17:36):

Hello.
I am working through "Theorem Proving in Lean" with only minimal background knowledge, so I am having trouble figuring out how to define curry and uncurry functions from the text:

def curry (α β γ : Type) (f : α × β → γ) : α → β → γ := sorry

def uncurry (α β γ : Type) (f : α → β → γ) : α × β → γ := sorry

The core of my confusion is that I do not understand how the return types α → β → γ and α × β → γ can be expressed.
Am I supposed to def a new function inside the given function definition? Trying that gives an error.

If I start with lambda x y z g (for types alpha, beta, gamma, and function f), I get x : alpha, y : beta, z : ?m_1, and f : ?m_1.

Would you please instruct me how to define these functions?

Thank you.

#### Edward Ayers (Sep 16 2019 at 17:41):

Hi! The answer is def curry (α β γ : Type) (f : α × β → γ) : α → β → γ := λ a b, f (a,b). In a def block, anything before the : is already in scope (so you don't need to lambda theα,β,γ or f ). If you replace sorry with an underscore _ and look at the lean output it will give you some hints about what is in scope and what the underscore needs to be replaced with.

#### Edward Ayers (Sep 16 2019 at 17:42):

So eg

def curry (α β γ : Type) (f : α × β → γ) : α → β → γ := _


Gives:

α β γ : Type,
f : α × β → γ
⊢ α → β → γ


#### Edward Ayers (Sep 16 2019 at 17:44):

So it's telling you that you need to provide a function that takes a α and β and returns a γ.

#### me myself and I (Sep 16 2019 at 17:47):

OK; I understand now.
lambda x y, f(x,y) is actually returning a function with the required signature, yes?
Thank you for your wise and timely assistance!

yep

#### Edward Ayers (Sep 16 2019 at 17:47):

np

Last updated: May 10 2021 at 18:22 UTC