> On Friday, May 26, 2023 at 11:10:02 PM UTC+2 David A. Wheeler wrote: > > Ask and ye shall receive!! As of this morning the first draft of the > metamath-lamp guide is available here: > https://github.com/expln/metamath-lamp/blob/master/docs/guide.md
> On May 27, 2023, at 10:17 AM, 'Alexander van der Vekens' via Metamath > <[email protected]> wrote: > I wanted to proof ( 5 + 7 ) = ; 1 2. Ouch, that's a worst case goal for metamath-lamp when compared to mmj2. The mmj2 tool has automations *specifically* for simple calculations like this, while metamath-lamp does not. But it's a valid goal, so carry on! > The replacement of a temporary variable is a little bit cumberson: if you > want to replace &C1 by 6, you cannot change it at one place (and then it is > replaced everywhere, as in mmj2), but you have to click A (apply a > substitution to all statements), then enter &C1 and 6 manually. In mmj2 you still need to manually replace the work variable (&C1) by its replacement somewhere (6). The current assumption in metamath-lamp is that for substitutions you'll always use the replacement command instead. That said, I think you're right, it would be better if metamath-lamp also allowed people to just edit a work variable into an expression and have unify automatically do the replacement. I've added that as a proposal here: https://github.com/expln/metamath-lamp/issues/43 > In the following, a second line with 5 e. NN0 was created (with the massage > This statement is the same as the previous one - '2' ) - at first, it was not > possible to get rid of it, I succeded, however, after a while... You should be able to select the statement & then choose "delete". If that didn't work, I'd love to know why. > At the end, I needed about one hour to finish the proof successfully (with > metamath.exe it was done within a few minutes). > To summarize, I think metamath-lamp is not stable/intuitive enough to be > suitable for a beginner at the moment. > > Finally, it would be very helpful if screen shots were available in this user > guide. Good point. In the long term I intend to create a video, just like I did with mmj2, but screen shots are still a good idea. Thanks for the feedback! I think you're right that metamath-lamp needs improvements in its UI & capabilities. However, I think some of that suggests a need to improve its documentation to clarify how to use it; mmj2 also has some oddities that work fine once you know what they are. I'm going to work on improving its documentation to hopefully make it easier. I still think it is helpful to have at least one tool that work "without an install" and can immediately work on smartphones. mmj2's automations and some specific mechanisms give it power that metamath-lamp currently lacks, but some people may be unwilling to go through the effort of installing a tool just to try it out. I'm hoping that metamath-lamp can be, at the least, a way to entice people into trying to create metamath proofs themselves. --- David A. Wheeler -- 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/94A90A04-E450-4228-A412-7060542EACA7%40dwheeler.com.
