Constructor expansion in argument of named def?

Stream: Is there code for X?

[James Oswald]

Rather than doing something like

structure S where
  a : Nat
  b : Nat

def add (s : S) : Nat := s.a + s.b

I am looking for a way to expand the constructor at the argument level, something like

 def add (⟨a, b⟩ : S) : Nat := a + b

I've tried a few different syntaxes, but nothing seems to work. This feels weird to me since using lambdas with this syntax seems to work fine.

#check λ (⟨a, b⟩ : S) => a + b

My real use case for this a structure with many levels of nested substructures, and I am trying to avoid the need to prefix with many levels of member accessors as it negatively impacts readability.

[Alex J. Best]

The closest I can think of is

structure S where
  a : Nat
  b : Nat

def add : (s : S) → Nat
| ⟨a, b⟩ => a + b

[Eric Wieser]

One possible explanation for why def add (⟨a, b⟩ : S) : Nat := a + b is not supported is that it prevents you naming the first argument; though I guess s@⟨a, b⟩ could be used to resolve that