Syntactic sugar to define function in struct + pattern match

Stream: lean4

[Théophile]

When defining a structure that contains a function, Lean allows to write f x := y instead of f := fun x => y.
Also, when writing a lambda, Lean allows to do a pattern matching on the parameters, for example fun (x, y) => z.
However, the two syntactic sugars cannot be combined, that is, when defining a structure it is invalid syntax to write f (x, y) := z. See example code below.

Is this "by design", or should I write an RFC to allow this syntax?

structure Test where
  f: (Nat × Nat) → Nat

def test1: Test := {
  f x := x.fst
}

def test2: Test where
  f x := x.fst

def test1': Test := {
  -- unexpected token ':='; expected '}'
  f (x, y) := x
}

def test2': Test where
  -- unexpected token ','; expected ')'
  f (x, y) := x

def test1'': Test := {
  f := fun (x, _) => x
}

def test2'': Test where
  f := fun (x, _) => x

[Kyle Miller]

It's by design. The syntax here is binder lists (like in a def, or tactics like let/have) rather than fun binders.

The syntax lets you use pattern matching like a def:

def test1': Test := {
  f | (x, y) => x
}

[Ruben Van de Velde]

I'm sad about the design though :)

[Théophile]

Okay, and it seems that this syntax is generic enough to handle multiple arguments (see code below), although it's a bit weird.

I wonder what is the deep reason behind this design choice though? Is it because otherwise there would be parsing ambiguities? Because it would be technically difficult (although doable) to do? Given the syntactic sugar that already exist in Lean, this one feels very natural and I'm surprised this doesn't work

structure Test where
  f: (Nat × Nat) → Nat → Nat

def test: Test where
  f | (x, y), z => x