On Sunday, July 14, 2019 at 10:30:04 PM UTC+3, fl wrote: > > Finally, I find that a system where the human-machine interface is very > visual is better. > > In short, that's why I think Metamath is not the best educational tool. >
But this isn't Metamth's fault in particular but merely mmj2's. And there must also be a preliminary sequence where the most frequent > reasonings and reasoning errors are explained on textual examples to keep > all this meaningful. > Right, that's where introductory texts should have their way. And any software assistant should have a feedback, i.e. red lines or shaded inaccessible rules. Present Metamath tools lack that, but it's irrelevant to language. -- 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/f5fb60fd-9e6c-4bcd-8a7d-a01291ceb0ee%40googlegroups.com.
