The Coq mailing list

["Randy Pollack" <rap AT dcs.ed.ac.uk>]

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).

Does the ordinary "Definition" allow such a shorthand?  If not, is
there a reason or can it be changed?

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

Thanks,
Randy