On Sunday, July 14, 2019 at 10:58:41 PM UTC+3, fl wrote: > > Mmj2 was designed as an editor to enter the proofs not as a pedagogical > tool. Don't blame it. It does its job perfectly. >
It might be a good editor but not so a good assistant. Good software should respect a separation of concerns, i.e. language should not leak to interface design and rendering of its results. Jape has been pretty good pedagogical tool because of that and nothing prevents Metamath from beating it. Mmj2 has a macro system implemented in Javascript, but I think it's pretty limited and never saw a tutorial for it. My hopes now lie with MM0/1 which should take these mistakes into account. -- 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/1abf453f-3dea-4a83-b717-4a26e5f5a89a%40googlegroups.com.
