pattern in def arguments

Stream: lean4

[James Gallicchio]

has there been any discussion about allowing (total) patterns in def argument lists? It is some nice syntax sugar, but low priority and I suspect not straightforward to implement

[Tomas Skrivan]

Do you mean something like this?

def add  := λ ((x,y) : Nat×Nat) => x + y -- this work

def add' ((x,y) : Nat×Nat) := x + y      -- this does not

[James Gallicchio]

or better yet, ((x : Nat), (y : Nat)) since that is also a valid pattern

[Tomas Skrivan]

Oh yeah that would be great! But I'm not aware of anything in this direction.

[James Gallicchio]

another common one would be being able to write () instead of (_ : Unit), which is getting a bit annoying to me :joy: