The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

On 11/11/2014 08:51 PM, Vadim Zaliva wrote:
> It looks like the paper, class SemiRing define differently from the
> actual definition in the library. According to the paper
> definition of SemiRing (page 10) I should be able to define Scalar
> Product of two vectors like this:
>
> Definition ScalarProd `{Semiring A}  {n} (a b: t A n) : A :=
>    fold_right (plus) (map2 (mult) a b) zero.
Try "SemiRing" with capital "R".

For what it is worth, I would only depend on the ring operations that 
you actually use, i.e.:

Definition ScalarProd `{Plus A, Zero A, Mult A}  {n} (a b: t A n) : A :=
  fold_right (+) (map2 (.*.) a b) 0.