Zulip Chat Archive

Stream: new members

Topic: Curry/Uncurry


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

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

view this post on Zulip Edward Ayers (Sep 16 2019 at 17:42):

So eg

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

Gives:

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

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

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

view this post on Zulip Edward Ayers (Sep 16 2019 at 17:47):

yep

view this post on Zulip Edward Ayers (Sep 16 2019 at 17:47):

np


Last updated: May 10 2021 at 18:22 UTC