You can use the "Renumber" option in the menu of mmj2 to get rid of "d" and other alphabetic naming. The ! steps should also go away once you have proved the step, meaning that complete proofs will hopefully not have these things. * comments though are ubiquitous in mmj2 proof worksheets and I don't know any method other than manually removing them if they cause problems.
But really, this all sounds like problems with eimm (which I don't know much about). Parsing the full syntax of mmj2-acceptable worksheets is a bit annoying because it is very forgiving of malformed steps, but I think it is reasonable to at least be able to support the kinds of worksheets that mmj2 actually generates. I would assume that it is just an out of date parser, since mmj2 was not always capable of parsing alphabetic step names, and did not always put !, although it has put * as long as I can remember. Mario On Wed, Apr 19, 2023 at 8:49 AM LM <[email protected]> wrote: > I am probably doing something wrong, but when I try using eimm it doesn't > like the .mmp saved by mmj2. > > the labels are expected to be purely numeric, while the autogenerated > labels have a 'd' prefix. > > it also fails to ignore * comments > > > I'm not sure how other people are using mmj2, and how they export/import... > > Greetings, > Ludwig > > -- > 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/207d31b0-3426-4620-8d78-089967874e72n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/207d31b0-3426-4620-8d78-089967874e72n%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/CAFXXJSvOzrp7J4-mD1esEE-%2BVvQEyHfRr3k6PaO9V7MdcvtumQ%40mail.gmail.com.
