You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Variable R : ringType.
Variable n : nat.
Implicit Types (p q r s : {poly R}).
Record truncfps := MkTfps { tfps : {poly R}; _ : size tfps <= n.+1 }.
HB.instance Definition _ : isSub _ _ truncfps := [isSub for tfps].
leads to
HB_unnamed_factory_1 is defined
Warning: Projection value has no head constant:
fun (K : truncfps -> Type)
(K_S : forall (x : {poly R}) (Px : (fun x0 : {poly R} => size x0 <= n.+1) x),
K (MkTfps Px)) (u : truncfps) =>
match u as u0 return (K u0) with
| @MkTfps x Px => K_S x Px
end in canonical instance HB_unnamed_factory_1 of isSub.Sub_rect, ignoring it.
[projection-no-head-constant,records,default]
tfps_truncfps__canonical__eqtype_SubType is defined
@cyrilcohen on zulip said: the canonical projections on non "keys" should be ignored. We should add a declaration of the form "canonical=false" when we declare mixin instances in hb.
The text was updated successfully, but these errors were encountered:
Here is an example:
leads to
@cyrilcohen on zulip said: the canonical projections on non "keys" should be ignored. We should add a declaration of the form "canonical=false" when we declare mixin instances in hb.
The text was updated successfully, but these errors were encountered: