coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Tool for exporting definitions, Luminous Fennell
- Re: [Coq-Club] Tool for exporting definitions,
Adam Chlipala
- Re: [Coq-Club] Tool for exporting definitions,
Luminous Fennell
- Re: [Coq-Club] Tool for exporting definitions,
Nuno Gaspar
- Re: [Coq-Club] Tool for exporting definitions,
AUGER Cédric
- Re: [Coq-Club] Tool for exporting definitions, Luminous Fennell
- Re: [Coq-Club] Tool for exporting definitions,
AUGER Cédric
- Re: [Coq-Club] Tool for exporting definitions,
Nuno Gaspar
- Re: [Coq-Club] Tool for exporting definitions,
Luminous Fennell
- Re: [Coq-Club] Tool for exporting definitions,
Adam Chlipala
Archive powered by MhonArc 2.6.16.