The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

> On Nov 11, 2014, at 12:49 , Robbert Krebbers 
> <mailinglists AT robbertkrebbers.nl>
>  wrote:
> 
>> Definition ScalarProd `{Semiring A}  {n} (a b: t A n) : A :=
>>   fold_right (plus) (map2 (mult) a b) zero.
> Try "SemiRing" with capital "R".

Thanks. It was a typo. Assuming I want to use a SemiRing class, how can I 
access plus,
mult and zero provided? I tried:

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

and got:

Error: Cannot infer the implicit parameter Plus of
plus.
Could not find an instance for "Plus A" in environment:

Sincerely,
Vadim Zaliva

--
CMU ECE PhD student
Mobile: +1(510)220-1060
Skype: vzaliva