Hello, I encountered a problem while defining the following.

```
Context {R: ringType} (U V: lmodType R).
Implicit Types (u v : {linear U -> V}).
Definition linear_zero : {linear U -> V} := [linear of 0].
Definition linear_neg u : {linear U -> V} := [linear of \- u].
Definition linear_add u v := [linear of u \+ v].
```

In particular, it errors out at `linear_neg`

with

```
The following term contains unresolved implicit arguments:
(fun u => [linear of \- u])
More precisely:
- ?l: Cannot infer an internal placeholder of type
"GRing.Scale.law (R:=R) (V:=V) *:%R" in
environment:
R : ringType
U, V : lmodType R
u : {linear U -> V}
```

The `lmodType`

structure on `V`

should provide the scale law.

In contrast, `linear_add`

one compiles and works well.

Why could this be happening?

That's a bug, sorry about that. I just submitted a fix: https://github.com/math-comp/math-comp/pull/917

Thanks a lot!!!

abab9579 has marked this topic as resolved.

Last updated: Jul 25 2024 at 16:02 UTC