HB.saturate fails on `Type`

math-comp / hierarchy-builder

High level commands to declare a hierarchy based on packed classes

MIT License

96 stars 21 forks source link

HB.saturate fails on `Type` #415

Open CohenCyril opened 7 months ago

CohenCyril commented 7 months ago

The following should succeed but does not

From HB Require Import structures.

HB.mixin Record HasPoint T := { default : T }.

HB.instance Definition _ A : HasPoint Type := HasPoint.Build Type nat.

HB.structure Definition Pointed  := { T of HasPoint T }.

HB.saturate.

(* This should succeed now *)
Check Type : Pointed.type.