Zulip Chat Archive

Stream: new members

Topic: Derive Field Accessors


view this post on Zulip 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)?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Pedro Minicz (Mar 05 2021 at 14:06):

Then @Logan Murphy's solution will work best.

view this post on Zulip 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}

view this post on Zulip Eric Wieser (Mar 05 2021 at 14:11):

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

view this post on Zulip Eric Wieser (Mar 05 2021 at 14:11):

Since extends X generates a to_X field for you

view this post on Zulip 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