OK I tried it again using 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 I wanted to proof ( 5 + 7 ) = ; 1 2. At the beginning, metamath-lamp did not give any helpful hint by itsself (you have to know some basic metamath theorems in advance), and often the prove action took very long (several minutes), even after I gave the hint that "6p5lem" can be used. In between, I was stuck when trying to prove ( 5 + 7 ) = ( ; 0 5 + ; 0 7 ) - I am not able to apply oveq12i to continue with using dec0h to complete this proof (step). 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 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... 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. -- 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/49da0362-62b7-4064-a09a-ce4194d9e18bn%40googlegroups.com.
