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 ?

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

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 !

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