Different function signatures

Stream: new members

[Brandon Brown]

Is there any difference between these two different function definition styles:

def add1 (a b : Nat) : Nat := sorry

def add2 : Nat → Nat → Nat := sorry

I intuitively understand that for add1 the sorry needs to be filled with a term of type Nat, whereas for add2 the sorry needs to be filled with a term of type Nat → Nat → Nat using a lambda term. But I don't know why I would prefer one over the other or why exactly the actual term definitions are different since both functions have the same type signature with #check

[Bryan Gin-ge Chen]

There's no difference once the definitions are complete, but sometimes one might be more convenient than the other when writing the term, e.g. if you want to use the equation compiler, you'll probably want to start with the latter.

[Kevin Buzzard]

but if you're doing a tactic proof (which would not be advisable here because it's a definition, but if these were predicates Nat -> Nat -> (some proposition)) then the advantage of the first one is that you don't have to start your proof with intros a b as you would have to with the second one

[Bryan Gin-ge Chen]

On the other hand, sometimes you want it in the latter form for tactic#induction.

[Brandon Brown]

I see, thanks you both