The Coq mailing list

[Vincent Siles <vincent.siles AT ens-lyon.org>]

Section myNat.
Parameter B: Set (* or Type, as you wish *)
Parameter plusB : B -> B -> B.

Definition some_code_using_B_and_plusB := .....

End myNat.

Check  some_code_using_B_and_plusB.

With this you will define your code with "plusB" as an argument, so that you 
can
feed it with plus for nat, or Z, or Q, or whatever has the type B -> B
-> B for some type B.

It is equivalent to directly write

Definition foo (B: Type) (plusB: B -> B -> B) (other args ...) := .....

Hope it helps,
V.

2012/4/30 Bernard Hurley 
<bernard AT marcade.biz>:
> 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?
>
> Cheers,
>
> Bernard.
>