The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 09/12/2014 08:10 AM, Ömer Sinan Ağacan wrote:
> I'm having trouble implementing even the simplest dependently typed
> term using `Fixpoint`, `Definition` etc. I've been doing a lot of
> proving using tactics lately and I'm very comfortable with tactics. So
> I thought why not define everything using tactics? I came up with
> this:

Have you read CPDT <http://adam.chlipala.net/cpdt/>? Certainly it is not 
obvious how to do dependently typed programming in Coq, but CPDT 
introduces techniques that should make it practical.  I claim it is 
almost always a bad idea to build honest-to-goodness programs using 
tactics for any part that has computational content.