The Coq mailing list

["John Wiegley" <johnw AT newartisans.com>]

>>>>> Craig McLaughlin 
>>>>> <mr_mcl AT live.co.uk>
>>>>>  writes:

> Thanks Jonathan! I was hesitant to use the proof mechanism to define
> functions for fear that the implementation would be much less efficient than
> PROGRAM.  However, it seems much easier to define dependently typed
> functions this way; in the past I also have tried the [refine] tactic but
> found it to be awkward to use for the impossible cases.

> Is there much consensus within the Coq community on the most favourable
> approach?

I don't know about consensus, but I _often_ use the proof mechanism for
defining functions involving dependent types or contradictions.  Only in a
very few cases has the extraction suffered enough to force me to rewrite the
proof term manually.

John