Stream: math-comp users

Topic: comoid from a zmodType


view this post on Zulip Florent Hivert (Nov 25 2023 at 22:53):

Before mathcomp2 one could get the addition law of a T : zmodType with

Let add_law := (add_comoid [zmodType of T])

Now with mathcomp2 I tried

Let add_law := (Monoid.ComLaw.on (+%R : T -> T -> T)).

However I got a Monoid.ComLaw.axioms_ 0 +%R where I would like to have a Monoid.com_law.
Any idea ?

view this post on Zulip Enrico Tassi (Nov 26 2023 at 06:56):

Try [the Monoid.com_law of ... ] or even Let add_law : Monoid.com_law .. := +%R : T -> ...

view this post on Zulip Florent Hivert (Nov 26 2023 at 07:23):

The first one doesn't work:

Let add_law := [the Monoid.com_law of TLim].

answers:

The term "Monoid.com_law" has type "forall T : Type, T -> Type"
which should be Set, Prop or Type.

But the second solution solves my problem:

Let add_law : Monoid.com_law 0 := (+%R : TLim -> TLim -> TLim).

Thanks !

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

I tried to fix the first solution but

Let add_law := [the Monoid.com_law 0 of TLim].

leads to

[...]
TLim : zmodInvLimType Sys
C : choiceType
s : Monoid.com_law 0
The term "s" has type "Monoid.com_law 0" while it is expected to have type
 "zmodInvLimType Sys".

Last updated: Jul 15 2024 at 21:02 UTC