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
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to