The Coq mailing list

[Bruno Barras <Bruno.Barras AT cl.cam.ac.uk>]

Hello Randy,


> As a functional programmer I like to write, e.g.
> 
> (1)   plus (n,m:nat) : nat = ...
> 
> rather than
> 
> (2)   plus : nat->nat->nat = \n:nat.\n:nat. ...
> 
> In Coq, the "Fixpoint" definition lets one write (1) instead of (2).

to avoid redundancy, you could write

Definition plus : nat->nat->nat := [n;m] ...

but I agree this is not as readable as what you would expect.
Anyway, as you have noticed, the Fixpoint notation is more friendly.
So, you can do

Fixpoint plus [n,m:nat]: nat := ...

If your definition is indeed not recursive, it will not generate the
useless fixpoint operator and it behaves like a definition.

> The notation I want almost exists, by using a Fixpoint with a dummy
> boolean argument.

I don't understand why you need this extra argument...

Bruno.