在 Lean Theorem Prover 中定义 `curry`

我正在阅读the official tutorial for Lean 3。我被困在 Chapter 2 中的第二个练习：

完成以下定义，其中“curry”和“uncurry”一个函数。

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

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

我目前的尝试是

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

这并不令人满意，因为我修改了练习中的类型，而不是仅仅用一些代码替换“sorry”。在保持类型相同的同时采取什么更好的方法？如果您能提供一些提示，而不是完整的解决方案，我将不胜感激。