Stream: Hierarchy Builder devs & users

Topic: Non canonical instance

view this post on Zulip Florent Hivert (Nov 24 2023 at 18:07):

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 ?

view this post on Zulip Florent Hivert (Nov 25 2023 at 09:11):

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 ?

view this post on Zulip Florent Hivert (Nov 25 2023 at 11:55):

I'm trying an it seems to work... So far...

Last updated: Apr 21 2024 at 01:02 UTC