IntersectMBO / formal-ledger-specifications

Formal specifications of the cardano ledger
Apache License 2.0
36 stars 13 forks source link

Don't parameterise the HasEmptySet class on a Theory #445

Closed UlfNorell closed 4 months ago

UlfNorell commented 4 months ago

Only the instances need a theory, so I split them out into Interface.HasEmptySet.Instances. With this change instance search doesn't have to consider the particular theory, only the set representation.

It does mean that we can't have different empty sets for different theories with the same underlying set representation, but I don't think that's something we are likely to need.