mixing positional and keyword arguments

Stream: lean4

[Julian Berman]

This isn't really a question, just something mildly interesting I just noticed -- in e.g. Python, doing foo(y=1, 2, 3) is a syntax error. But in lean:

def foo (x : Nat) (y : Nat) (z : Nat) := x + y + z
#check foo (y := 1) 2 3

where lean4 happily seems to reorder arguments so that the positional ones are all the filled in arguments you didn't pass by name.

[Kevin Buzzard]

Yes, IIRC this is mentioned in the manual

[Julian Berman]

nod -- there are examples shown of it here yeah: https://leanprover.github.io/lean4/doc/lean3changes.html#function-applications though I didn't catch it from the prose text