Skip to Content.
Sympa Menu

coq-club - [Coq-Club] An attempt to revive the "Show Tree" command.

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] An attempt to revive the "Show Tree" command.


Chronological Thread 
  • 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.

Top of Page