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

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