Record inheritance

[re-xyr]

trafficstars

How to do this? In Lean, if structure a extends b, then we can build a by either { to_b := some_b_instance, <fields of a> } or { <fields of b>, <fields of a> }. When accessing some b field in an a instance, we can either use a.field or a.to_b.field.

[ice1000]

We need to implement aya-prover/aya-prover-proto#150 (which, I guess, is related to aya-prover/aya-prover-proto#128) first

[re-xyr]

So we should implement in this order:

• typeclass w/o inheritance
• coercion as typeclass
• record inheritance through coercion
• typeclass inheritance through record inheritance

[ice1000]

... and built-in definitions.

[ice1000]

I mean pragmas that make definitions interact with built-in features

[ice1000]

So we should implement in this order:

• typeclass w/o inheritance
• coercion as typeclass
• record inheritance through coercion
• typeclass inheritance through record inheritance

No, in this order:

• aya-prover/aya-prover-proto#503
• as listed above

[ice1000]

In Arend, they have this:

class Functor F
 | bleh

class Monad F extends Functor
 | blah

instance ok : Functor Bla
 | bleh

instance ko : Monad Bla
 | Functor => ok
 | bleh => *&^%$#$%^&