coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] proof tree visualization

From: Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>
To: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] proof tree visualization
Date: Mon, 2 May 2011 16:42:05 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type; b=Rf+TIsBk+ycJI0qKUkmP7vaWEoBOLJw8A/QDnClzvT2kQyZfjYDzx4DUE3DIJdcCiL AW33J12CxHO8rBfGYoS3v0RBqwLhTM3wxuuikhk/Cw0Abr/ZgTShw1AoGzWTAMTHdfis M6ZlBBO2JKNQVGjFFxq+htv4xiw5bovwzLztY=

2011/5/2 Arnaud Spiwack
<aspiwack AT lix.polytechnique.fr>:
> None of these are promises. Rather things I'm willing to spend some time
> thinking of at some point.

That's at least a good start :)

I would just like to insist that the current version of the bullets
(as I understand them) does not really help to deal with very big
inductives (say with 39 constructors like that one
http://compcert.inria.fr/doc/html/Csem.html#sstep ;), when after an
induction, a tactic closes half of the cases. I hope you will have
good ideas on that!

Keep us posted

Alexandre

Re: [Coq-Club] proof tree visualization, Alexandre Pilkiewicz
- Re: [Coq-Club] proof tree visualization, Arnaud Spiwack
  - Re: [Coq-Club] proof tree visualization, Alexandre Pilkiewicz