## Stream: lean4

### Topic: mixing positional and keyword arguments

#### Julian Berman (Feb 27 2021 at 20:57):

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 (Feb 27 2021 at 21:38):

Yes, IIRC this is mentioned in the manual

#### Julian Berman (Feb 27 2021 at 21:49):

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

Last updated: May 18 2021 at 23:14 UTC