In sort of the same vein, in Coq, we have named hypotheses in our
proof contexts which render like:
Hyp0 : Hyp (P x)
Hyp1 : Hyp (P z)
============================
or (P x) (or (forall y : U, P y) False)
I'd like to add some PGML so that it looks something like this:
<proofstate>
<hypotheses>
<hyp>Hyp0 : Hyp (P x)</hyp>
<hyp>Hyp1 : Hyp (P z)</hyp>
</hypotheses>
<goal>
or (P x) (or (forall y : U, P y) False)
</goal>
</proofstate>
But I don't know what the right PGIP/PGML tags are.
Edward
Excerpts from Edward Z. Yang's message of Thu Apr 05 23:15:50 -0400 2012:
> Hello all,
>
> I'm working on partial PGIP support Coq, and one thing that I would like
> to support is the case when Coq outputs "warning" messages, of which
> there are many but which are nonfatal. I'm wondering what the right
> tag for these are. <errorresponse> is not correct, because we're only
> allowed to have one before <ready/>. Is <metainforesponse> correct?
> It seems too generic, and where am I supposed to attach other metadata?
>
> Cheers,
> Edward
_______________________________________________
ProofGeneral-devel mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
