The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

On 08/03/2015 12:56 PM, Pierre Courtieu wrote:
> (...) I think that having a strict document structure is important.
> For scalability, tooling, documenting etc. nested lemmas as they are
> currently implemented is a serious hole in this structure.

A possible counter argument regarding the tooling argument: in company-coq, 
you can press C-c C-a C-x to extract the current goal and some hypotheses to 
a separate lemma, and start proving it right away. I find that very useful 
for using Coq in an exploratory manner: I start without a clear idea of what 
lemmas I need, and every time I reach a goal that looks interesting I extract 
it to a lemma, with just the relevant hypotheses. Being forced to rewind the 
current proof and move this sub-lemma up in the document would make this 
workflow a lot less convenient.

Cheers,
Clément.

Attachment: signature.asc
Description: OpenPGP digital signature