Stream: math-comp users

Topic: Cannot use existing linear structure of `\- u`

view this post on Zulip abab9579 (Sep 05 2022 at 02:03):

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
  " (R:=R) (V:=V)  *:%R" in
  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?

view this post on Zulip Pierre Roux (Sep 05 2022 at 11:52):

That's a bug, sorry about that. I just submitted a fix:

view this post on Zulip abab9579 (Sep 05 2022 at 11:58):

Thanks a lot!!!

Last updated: Feb 08 2023 at 04:04 UTC