Hi Glauco,
In MMJ2, here are some methods for mmj.pa.ProofStepStmt
<https://github.com/digama0/mmj2/blob/master/src/mmj/pa/ProofStepStmt.java>:
public String getStepName();
public String[] getHypSteps();
public void setRef(Stmt ref);
public Stmt getRef();
public String getRefLabel();
public Formula getFormula();
public boolean isHypothesisStep();
public boolean isDerivationStep();
So:
* "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).
Any documentation about MMJ2 should be here:
https://github.com/digama0/mmj2/tree/master/doc
In metamath-vspa, I've been using similar names.
BR,
_
Thierry
On 25/04/2022 21:25, Glauco wrote:
Is there a formal spec for the mmp format? An EBNF like what we can
find in Appendix E (of the Metamath book) for the mm spec?
I've a Typescript parser/verifier for .mm/.mmp files that's working
pretty well, but I'm adding new features, and I would like to
standardize the names of Classes/Properties/Methods to an "official" spec.
If a BNF is not available, is there a "standard" name for the "blob"
at the beginning of any mmp statement, I mean, this guy here
72:71,70:mpbid
(I've looked at some mmj2 source code, but I've not been able to
easily find a place where that blob is referenced with a name)
Thanks in advance
Glauco
Il giorno martedì 15 febbraio 2022 alle 03:40:33 UTC+1 Thierry Arnoux
ha scritto:
Hi Glauco,
MMJ2-style unification is certainly a goal! Many building blocks
for this are actually already in place - not all, but we’re slowly
getting there.
An even more remote goal would be to use this framework to build a
more tactics-based proof assistant, but that’s in a much more
distant future!
Right now Metamath-knife’s API is still changing (and I expect it
to continue). One thing you’ll have to take care about if building
metamath-vspa is to use the correct version. I hope we fix that soon.
Any help is certainly welcome! The choice of Rust was discussed in
this forum a while ago, one motivation being that Ralph and Mario
both master it. I’ve been self-learning Rust, I still am not very
good and I certainly still have a lot to learn, but I had a lot of
fun learning it. It has a lot of features I was hoping for when
programming in C.
Each editor function (diagnostics, completion, references, search,
formatting, etc.) is a different functionality which can be built
in parallel and stay relatively independent, so it shall be very
feasible to have several people working together on that project.
BR,
_
Thierry
> Le 15 févr. 2022 à 03:54, Glauco <[email protected]> a écrit :
>
> Thierry, this is so cool!
>
> Is a mmj2 ctrl+u like action available? Please, feel free to ask
if you need help with this one (I don't know anything about Rust,
but it's now on top of my list of things to learn)
>
> Can't wait to build and try it!
>
> 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/7e84b4c0-e4f4-409b-b54d-4d51f4edaf74n%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/7e84b4c0-e4f4-409b-b54d-4d51f4edaf74n%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/21723121-fbe6-2d8e-9ba6-ddc4fc18cb9d%40gmx.net.
