lean book

Stream: new members

[Brandon B]

I'm going through "Theorem Proving in Lean" and I'm on page 19 where it has a little exercise to finish writing the curry and uncurry functions.
If I start with what is written in the book:

def curry (α β γ : Type) (f : α × β → γ) : α → β → γ := λ a b, f (a,b)
def add (a : ℕ × ℕ) : ℕ := a.1 + a.2
#check curry add

It doesn't type check, but if I replace the parentheses of (α β γ : Type) to curly braces {α β γ : Type} then it works. Is this a typo in the book or am I misunderstanding something?

[Bryan Gin-ge Chen]

Are you looking at a PDF file? I don't see #check curry add in the more up-to-date web version.

[Brandon B]

No I added the last two lines to verify that my curry function can curry a simple add function originally defined on the cartesian product two natural numbers

[Daniel Keys]

The first three arguments to curry are the three types: alpha, beta, gamma.

[Daniel Keys]

The way you wrote it.

[Bryan Gin-ge Chen]

Oh, then yeah, changing curry to use implicit arguments as you did is probably best. I think the only reason α β γ are explicit there is that implicit arguments aren't introduced until 2.9. As Daniel Keys says, if you want #check to work with the original version, you'd write it this way:

def curry (α β γ : Type) (f : α × β → γ) : α → β → γ := λ a b, f (a,b)
def add (a : ℕ × ℕ) : ℕ := a.1 + a.2
#check curry ℕ ℕ ℕ add

[Daniel Keys]

If you replace the parantheses with braces, these arguments become implicit.
OK, see the answer from @Bryan Gin-ge Chen who was faster.

[Brandon B]

Ohhh that makes sense, thanks!