The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Sunday, April 29, 2012 11:18:09 PM Bernard Hurley wrote:
> Hi.
> 
> I have a set [B] with and a Fixpoint [plus_B:B->B->B]. I also have a lot
> of code written in two parts that are identical except that in one I am
> using [nat] and [plus] and in the other I am using [B] and [plus_B]. Is
> there any way of writing this polymorphically?

Class Plus (X Y Z:Type) : Type :=
| plus : X -> Y -> Z.

Class PlusOp (X:Type) : Type :=
| plus_op :> Plus X X X.

Infix "+" := plus.

Require Import ZArith.

Instance : PlusOp nat := Peano.plus.
Instance : PlusOp positive := Pplus.
Instance : PlusOp N := Nplus.
Instance : PlusOp Z := Zplus.

Check (2 + 3).
Check (2%positive + 3%positive).
Check (2%N + 3%N).
Check (2%Z + (-3)%Z).

Section my_stuff_with_general_plus.

Variable B:Type.
Context `{PlusOp B}.

...

End my_stuff_with_general_plus.
-- 
Daniel Schepler