Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Printing a structured representation of a Prop?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Printing a structured representation of a Prop?


Chronological Thread 
  • From: Clément Pit--Claudel <clement.pit AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Printing a structured representation of a Prop?
  • Date: Thu, 02 Jul 2015 01:13:45 -0700

Thanks! That's extremely helpful.

On 07/01/2015 11:23 PM, Valentin Robert wrote:
> <call val="Init"><option val="none"/></call>
> <value val="good"><state_id val="1"/></value>
>
> <call val="Add">
> <pair>
> <pair>
> <string>Theorem t : forall n, 0 + n = 0.</string>
> <int>0</int>
> </pair>
> <pair>
> <state_id val="1"/>
> <bool val="false"/>
> </pair>
> </pair>
> </call>
> <value val="good"><pair><state_id val="2"/><pair><union
> val="in_l"><unit/></union><string></string></pair></pair></value>
>
> <call val="PrintAst"><state_id val="2"/></call>
> <value val="good"><gallina begin="0" end="32"><theorem begin="0" end="32"
> type="Theorem" name="t"><apply begin="12" end="31"><operator begin="12"
> end="31" name="forall"/><constant begin="19" end="20" name="n"/><apply
> begin="22" end="31"><operator begin="22" end="31" name="_ = _"/><apply
> begin="22" end="27"><operator begin="22" end="27" name="_ + _"/><token
> begin="22" end="23">0</token><constant begin="26" end="27"
> name="n"/></apply><token begin="30"
> end="31">0</token></apply></apply></theorem></gallina></value>
>
> <call val="Quit"><unit/></call>



Archive powered by MHonArc 2.6.18.

Top of Page