coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
- To: coq-club AT inria.fr
- Cc: Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>
- Subject: Re: [Coq-Club] proof tree visualization
- Date: Mon, 2 May 2011 14:22: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=wh2BT0j7JhA7PaOg/5a05tHSd1YpkDneGUWag0XkKbDXN08eP+4cUhF3Dke9u6wQxM +7cvbiPdyjoao5XClCeGoeoShKkwJAHmlsmgZJMkpjSzoJnyDPWiXYjVYGbbGy4eePZN +92gYxr+B/m7xPlr3YWM2aXzXu4MS5+uVZQ5E=
Well, I cannot be very specific but I was thinking of
1/ Building on bullets (currently experimental) for robust proofs. There is also (already in trunk) BeginSubproof and EndSuproof keywords (the names may change) which have similar effect. Other keywords/semantics can be readily implemented if there is some support for it.
2/ Facilities for naming goals. I haven't thought much of a final form for this.
3/ Extra beefy destruction tactics, with syntax such as: Destruct n. Case S 0. […] Case 0. […] Case S (S p). […]
2/ Facilities for naming goals. I haven't thought much of a final form for this.
3/ Extra beefy destruction tactics, with syntax such as: Destruct n. Case S 0. […] Case 0. […] Case S (S p). […]
None of these are promises. Rather things I'm willing to spend some time thinking of at some point.
Arnaud
On 1 May 2011 00:22, Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org> wrote:
Hi Arnaud
2011/4/29 Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>:
> It is quite likely that such features make their way to Coq. Though not forDo you have any details on that? What sort of plans? I'm not talking
> the next release I'm afraid.
about a time line, just to have an idea of what kind of feature we can
expect. Are you talking about the bullets, or something more advanced?
I would really love to have more informations!
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
- Re: [Coq-Club] proof tree visualization, Arnaud Spiwack
Archive powered by MhonArc 2.6.16.