The Coq mailing list

[Patrick Loiseleur <Patrick.Loiseleur AT lri.fr>]

Dans son message du Monday 15 February, Randy Pollack a écrit : 
> Hi Bruno,
> 
> rap> The notation I want almost exists, by using a Fixpoint with a dummy
> rap> boolean argument.
> 
> barras> I don't understand why you need this extra argument...
> 
> I was misled by the manual (p.35) which says the type of the recursive
> variable should be inductively defined.  I was using a dummy boolean
> just to have some inductive argument.
> 
> Still, it would be better to make "Definition" accept parameters.
> 
> Thanks,
> Randy

It is a good idea to accept the syntax :

Definition f [n:nat; m,x:bool] := ...

because it is symmetric with the "Fixpoint" command.

I remember this point was discussed in the Coq team, but it wasn't
implemented.

It will be added in the next release. People that cannot wait should
send me a note and they will receive a patch against the 6.2.4

Best regards,

PL

-- 
Patrick.Loiseleur AT lri.fr