We (@mkerjean ) were surprised that the following didn't work:
From HB Require Import structures.
From mathcomp Require Import all_ssreflect ssralg ssrnum.
Section scale_law_raddf0.
Context {R : numDomainType} {E F : lmodType R} {s : GRing.Scale.law R F}.
Import GRing.Theory.
Lemma try_raddf0 : linear_for s ((fun=> 0%R) : E -> F).
Proof.
move => r x y /=.
Fail rewrite raddf0.
Abort.It looks as if GRing.Scale.law doesn't have the additive structure by default:
From mathcomp Require Import all_ssreflect ssralg ssrnum.
Section scale_law_raddf0.
Context {R : numDomainType} {E F : lmodType R} {s : GRing.Scale.law R F}.
Import GRing.Theory.
Lemma try_raddf0 : linear_for s ((fun=> 0%R) : E -> F).
Proof.
move => r x y /=.
Fail rewrite raddf0.
Abort.
Lemma it_is_additive r : @Algebra.isNmodMorphism F F (s r).
Proof.
split.
by apply: GRing.Scale.op_nmod_morphism.
Qed.
HB.instance Definition _ r := it_is_additive r.
Lemma try_raddf0 : linear_for s ((fun=> 0%R) : E -> F).
Proof.
move => r x y /=.
by rewrite raddf0 addr0.
Qed.
End scale_law_raddf0.Did we for example forget to open a namespace? @pi8027 @CohenCyril
We (@mkerjean ) were surprised that the following didn't work:
It looks as if
GRing.Scale.lawdoesn't have the additive structure by default:Did we for example forget to open a namespace? @pi8027 @CohenCyril