Glauco, > But I believe that Yamma is at least as cumbersome as mmj2 :-)
Yamma looks very cool, but it requires VSCode (and I'm on linux...), so I agree that it is perhaps easier to get mmj2 going. Igor, > For syntax check you also can use mm-lamp. Thanks for checking the file! Mm-lamp looks very promising. I tried checking some statement in your proof assistant, and, I'm probably going to express a common remark, but I wish it was possible to type proofs in text there as in mmj2, instead of clicking through GUI. Nice tool, in any case! -- 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/15a5930b-0b93-4de4-85ff-c4b74f1afe99n%40googlegroups.com.
