The Coq mailing list

[Bernard Hurley <bernard AT marcade.biz>]

Thanks, that's a very nice way of doing it!

Bernard.

On Mon, Apr 30, 2012 at 09:50:40AM -0700, Daniel Schepler wrote:
> 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