Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Tool for exporting definitions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Tool for exporting definitions


chronological Thread 
  • From: Luminous Fennell <mstrlu AT gmx.net>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Tool for exporting definitions
  • Date: Thu, 12 Jan 2012 17:01:57 +0100

I sent this mail before, but it didn't seem to have come through... I'm
sorry if I'm mistaken and this is a double-post:

Hello list,

Over the holidays, I wrote some Haskell code to export Coq definitions
to LaTeX or ASCII documents. It's basically an xml parser and some
combinators to format/pretty-print the resulting AST. It's also not
documented and not very general (yet). I plan to use it for my master's
thesis (I'm a CS student into programming languages), in order to easily
print out and think about my newest type-system/semantics attempts,
without to type everything multiple times.

My questions is, if it would be worth it to put a little bit more effort
in this (i.e. making a real project out of this). Is there already such
a tool? And if not would anybody else be interested or find this useful?

I know about Ott, but it seems useful to me to export from Coq directly.

I know that HELM exists, but I couldn't even get past the front page
(http://helm.cs.unibo.it/library.html). I get ``cannot connect'' or 403
errors (Is there some good instructions anywhere how to use HELM?)

Best regards

Lu



Archive powered by MhonArc 2.6.16.

Top of Page