coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Machine-parseable format for Coq terms

From: Stéphane Glondu <steph AT glondu.net>
To: "Edward Z. Yang" <ezyang AT mit.edu>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Machine-parseable format for Coq terms
Date: Thu, 05 Apr 2012 15:09:09 +0200

Le 04/04/2012 21:05, Edward Z. Yang a écrit :
> Is there a nice, easy to parse format for Coq terms (e.g. "or False (or
> False
> (or False (or (((A -> B) -> A) -> A) False)))" or Set Printing All on
> steroids)? I am building a parser for a fragment of the Coq term language
> (since this doesn't involve patching Coq), but it would be much nicer if I
> could get everything in a nicer format.

Print XML

Cheers,

--
Stéphane

[Coq-Club] Machine-parseable format for Coq terms, Edward Z. Yang
- Re: [Coq-Club] Machine-parseable format for Coq terms, Stéphane Glondu
  - Re: [Coq-Club] Machine-parseable format for Coq terms, Edward Z. Yang
    - Re: [Coq-Club] Machine-parseable format for Coq terms, Stéphane Glondu