Zulip Chat Archive

Stream: lean4

Topic: mixing positional and keyword arguments


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 27 2021 at 21:38):

Yes, IIRC this is mentioned in the manual

view this post on Zulip 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