EasyCrypt / easycrypt

EasyCrypt: Computer-Aided Cryptographic Proofs
MIT License
318 stars 49 forks source link

[TC] Allow instantiation of type classes defined by extension #515

Open fdupress opened 9 months ago

fdupress commented 9 months ago

Consider

type class monoid = {
  op idm : monoid
  op (+) : monoid -> monoid -> monoid

  ...
}.

type class group <: monoid = {
  op [-] : group -> group

  ...
}.

It is currently only possible to instantiate [-] when defining an instance of group, even if an instance of monoid exists. (Ideally, we would want to be able to define the instance of group directly. But defining it by explicit extension of an instance of monoid would be fine as well.)