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: Oct 13 2024 at 01:02 UTC