Pattern matching in function head

Stream: lean4

[James Sully]

Is there any particular reason irrefutable patterns aren't allowed in function parameters? I find myself regularly doing refactors like this when I don't want to name parameters:

def myFst (prod : α × β) : α :=
  match prod with | (a, _) => a

def myFst' : (α × β) → α
  | (a, _) => a

Reconfiguring the whole type signature each time is a mild pain. I'd like to be able to write

def myFst ((a, _) : α × β) : α := a

[Max Nowak 🐉]

I low-key also wish this was possible, at least for obvious single-constructor types. Also, you don't need a whole match, you can just do let (a, _) := prod.

[James Sully]

Max Nowak 🐉 said:

you can just do let (a, _) := prod.

Oh yeah, good point