The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 03/10/2013 11:07, Fabien Renaud wrote:
> I think I will use Function since I don't actually need any Program's
> features and I now understand how to use it.

Just for the reminder: using Function may seem appealing at first, and
can be sufficient in some cases, but it has some drawbacks.

In particular, it will often hide you the fact that you could get rid of
it by choosing a better-fitted data structure to induce on. Hence it may
prevent you from building nice and elegant proofs. Plus it is hell on
earth to compute with, as it provides you with horrendous terms.

I do not know why a bunch of people on Coq-club is supporting Function
use, but I would not recommend using it myself to beginners-ish.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature