The Coq mailing list

[Bernard Hurley <bernard AT marcade.biz>]

Thanks Vincent, that's very useful!

Bernard.

On Mon, Apr 30, 2012 at 08:39:05AM +0200, Vincent Siles wrote:
> 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.
> >