I had before mathcomp 2 some instances that I didn't want to make canonicalin general, but give the user to possibility to do so on specific examples. Precisely, any inverse limit of Zmodule in the category of Set naturally acquire a Zmodule structure. However, It may have a already a different Zmodule structure. So this invlim_zmodInvLimType
wasn't canonical before. With mathcomp2 If I try to define it is complains about non forgetful inheritance. I used to define a proper mixin in a module and allow the user to get it through a notation:
Notation "[ 'zmodMixin' 'of' U 'by' <- ]" :=
(InvLimitZmod.invlim_zmodMixin (Phant U))
(at level 0, format "[ 'zmodMixin' 'of' U 'by' <- ]") : form_scope.
So that one could later write
Local Canonical TLim_zmodType :=
Eval hnf in ZmodType TLim [zmodMixin of TLim by <-].
Is there an equivalent of that in mathcomp2 ?
I just realize this morning that this could probably be done with a builder/factory : InvLim_isZmodInvLim. Do you think this is a right way to go ?
I'm trying an it seems to work... So far...
Last updated: Oct 13 2024 at 01:02 UTC