Hi Glauco,
I think I found what you're looking for:
http://mmj2-doc.tirix.org/doc/ProofAssistantGUIDetailedInfo.html
<http://mmj2-doc.tirix.org/doc/ProofAssistantGUIDetailedInfo.html>
As far as I'm concerned I only have a difference at the level of the
proof step, and then these components, so I did not have to name that
"prefix".
The comments in ProofWorksheet.loadWorksheet
<https://github.com/digama0/mmj2/blob/8f49fb2c93531c5c75fcb65886837c8d0617c033/src/mmj/pa/ProofWorksheet.java#L1025>contain
some information about what is being checked when loading a proof step,
but it is not a definition either.
It could be useful to have such a definition of what a "Metamath Proof
File" is. My previous Eclipse plugin (which was a shell around MMJ2)
used the same format, *metamath-knife* can output that format, and I'm
starting to use the exact same format in *metamath-vspa*.
Maybe we could simply write a ".MD" markdown file in set.mm for filling
that purpose?
BR,
_
Thierry
On 25/04/2022 23:47, Glauco wrote:
Hi Thierry,
* "StepName" would be the name of the step, "72" in your example,
* "HypSteps" would be the essential hypotheses, "71,70" in your
example,
* "RefLabel" would be the label of the theorem applied, like
"mpbid",
* and "formula" is the formula itself (not shown in your example)
I've come up with names for the single "components" of the blob, and
the formula, but I was looking for a "name" for the whole blob (from
the standpoint of my WHITESPACE based tokenizer, it's the first token
of a mmp statement, when present; then of course another parser breaks
this token down to its components).
Are you aware of a formal syntax description of .mmp files?
Thanks again
Glauco
--
You received this message because you are subscribed to the Google
Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send
an email to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/4d2b9eb5-5fbb-4a6e-b69f-1045f6806de2n%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/4d2b9eb5-5fbb-4a6e-b69f-1045f6806de2n%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/4a64ad66-71b6-8087-23b9-4ee607d756de%40gmx.net.
