## Stream: new members

### Topic: Derive Field Accessors

#### Marcus Rossel (Mar 05 2021 at 13:24):

If I have ...

structure S :=
(a : int)
(b : int)


... and then define a wrapper

structure W :=
(s : S)
(p : s.a + s.b = 0)


... then is there a way for W to inherit accessors to the fields of s, so that I can just write w.a and w.b (w : W)?

#### Logan Murphy (Mar 05 2021 at 13:59):

Does something like

namespace W

def a (w : W) : int := w.s.a

end W

variable (w: W)

#check w.a


work?

#### Pedro Minicz (Mar 05 2021 at 14:00):

structure S :=
(a : int)
(b : int)

structure W extends S :=
(p : a + b = 0)

variable w : W

#check w.a


#### Marcus Rossel (Mar 05 2021 at 14:04):

Pedro Minicz said:

structure S :=
(a : int)
(b : int)

structure W extends S :=
(p : a + b = 0)

variable w : W

#check w.a


I still want W to have the field s.

#### Pedro Minicz (Mar 05 2021 at 14:06):

Then @Logan Murphy's solution will work best.

#### Marcus Rossel (Mar 05 2021 at 14:08):

I just noticed that a reverse approach might work well:

structure S :=
(a : int)
(b : int)

structure W extends S :=
(p : a + b = 0)

def W.s (w : W) : S := {a := w.a, b := w.b}


#### Eric Wieser (Mar 05 2021 at 14:11):

Or just def W.s (w : W) : S := w.to_S

#### Eric Wieser (Mar 05 2021 at 14:11):

Since extends X generates a to_X field for you

#### Marcus Rossel (Mar 05 2021 at 14:14):

Eric Wieser said:

Since extends X generates a to_X field for you

Oh perfect!

Last updated: May 14 2021 at 23:14 UTC