coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] An attempt to revive the "Show Tree" command.
- Date: Sat, 18 Jul 2015 21:53:13 +0200
Hi there,
This is somewhat controversial topic.
Recently, I was speculating how to revive the "Show Tree" command:
https://coq.inria.fr/refman/Reference-Manual009.html#hevea_command219
For those proofs that conform to certain restrictions
(no nested proofs, no bullets, no "<number> : <tactic>", ...)
I think the "Show Tree" command can provide meaningful output.
The motivation is described here:
http://217.67.21.78/doc/coq/coq-8.5-hack/index.html
Whoever is interested in this kind of thing, let me know.
I know about some of the things that must be finished
(like error handling)
Ultimately, I am mostly curious about whether this (or what)
might enable me to talk about Coq proofs with people who did not study Coq
(specifically).
At the end of the page linked above are installation instructions.
PS: big thanks to the people at Coq Coding Sprint for giving me some of the
essentials clues
(how Coq internally represents proof scripts)
- [Coq-Club] An attempt to revive the "Show Tree" command., Matej Kosik, 07/18/2015
Archive powered by MHonArc 2.6.18.