How to define curry in Lean

Question

I just started with Lean and with this nice SE.

In the official web book/tutorial, when explaining definitions https://leanprover.github.io/theorem_proving_in_lean/index.html they ask to complete this (partial) definition of curry (in paragraph 2.4):

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

I tried

def curry (α β γ : Type*) (f : α × β → γ) : α → β → γ := λ  x y, f (x,y) 

and it seems to be accepted by the system.

Is this definition correct? If yes, how do I use it?

I expected something like

curry x y f or curry f x y

should work, but they don't.

Actually the given (partial) definition is of type α → β → γ so it expects just 2 arguments of type α and β respectively, but no function f.

Thank you for your help

Answer 1

If Lean checks your code you know it is correct. (Well, that and the fact there is only one curry function up to functional equivalence.)

Now as for how to use curry you just defined, notice the type signature says you need to put in the following things in order:

• α : Type*
• β : Type*
• γ : Type*
• f : α × β → γ
• x : α
• y : β

So you have to use it as, e.g.

curry ℕ bool ℤ f n b

---

Note, it is cumbersome to have to write the types since you can usually get them from the types of f, n, and b in this case. So usually (and the tutorial will get to this soon), you write this function using curly braces for the arguments which are implicit:

def curry' {α β γ : Type*} (f : α × β → γ) : α → β → γ := λ  x y, f (x,y)

In this case, you can write this as

curry' f x y

or in rare cases when you need to supply the types:

@curry' α β γ f x y