Derive Field Accessors

Stream: new members

[Marcus Rossel]

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]

Does something like

namespace W

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

end W

variable (w: W)

#check w.a

work?

[Pedro Minicz]

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

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

variable w : W

#check w.a

[Marcus Rossel]

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]

Then @Logan Murphy's solution will work best.

[Marcus Rossel]

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]

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

[Eric Wieser]

Since extends X generates a to_X field for you

[Marcus Rossel]

Eric Wieser said:

Since extends X generates a to_X field for you

Oh perfect!