Misunderstanding default arguments

Stream: lean4

[Horatiu Cheval]

Suppose I have something like

def f (default : Nat := 0) : Nat → Nat := fun n => default + n

Then, #check f shows f 0 : Nat → Nat as I would expect, but if I try to apply it as in #check f 4 I still get a function, whereas what I expected was a Nat (i.e. f 0 4 : Nat). What am I doing wrong?

[Horatiu Cheval]

Oh, nevermind, I just needed parantheses #check (f) 4 is indeed a f 0 4 : Nat.

[Sebastian Ullrich]

Haha, I didn't know that worked

[Sebastian Ullrich]

Usually default parameters should only be declared after non-default parameters

[Horatiu Cheval]

Yeah, that makes a lot more sense now that you're saying it