The Coq mailing list

[gallego AT cri.ensmp.fr (Emilio Jesús Gallego Arias)]

Hi Clément,

Clément Pit--Claudel 
<clement.pit AT gmail.com>
 writes:

> Is there a way to print a structured representation of a lemma's
> statement in Coq? Ideally I'd like to get something like (forall ((A
> type) (x A) (y A)) (impl (eq x y) (eq y x))) given the lemma [forall A
> (x y: A), x = y -> y = x].
>
> * Basic extracting to JSON doesn't do, because Props are erased before 
> extraction.
> * The PrintAst XML command looks promising, but I'm not sure what its 
> syntax is. [1]
> * The code in texmacspp.ml also looks promising, but I have no idea how to 
> call into it.

That's very interesting, please let us know if you make any progress.

In our case, we resorted to linking directly to Coq (I happen to be in
Ocaml-land).

I just can't see how to do some of the more advances interaction/display
features we have in mind just using the protocol.

Best,
E.

Attachment: signature.asc
Description: PGP signature