The Coq mailing list

[Bas Spitters <spitters AT cs.ru.nl>]

On Wednesday 16 September 2009 17:04:34 Adam Chlipala wrote:
> Bas Spitters wrote:
> > Is there a pretty printer for coq sources?
> > I would be especially interested in having a tool for indentation.
> >
> >
> > n-1 leading spaces for n open goals. This makes proof scripts easier
> > to maintain.
>
> If your proof scripts are deeply nested enough for you to want to use
> indentation to indicate nesting depth, then you should probably be
> breaking your proofs into more lemmas that you add as proof hints. ;)

I am trying to maintain old proofs.

> I purposely don't believe that proof scripts with non-trivial nesting
> can ever be easy to maintain, regardless of how you display them. I
> recommend using automation to prove every theorem with a single tactic.
> There are examples of this kind of proof in two projects that I've
> worked on recently:
> http://ltamer.sourceforge.net/
> http://ynot.cs.harvard.edu/
> ...and I try to explain how to do it in this book-in-progress:
> http://adam.chlipala.net/cpdt/

Thanks,

Bas