> > > Finally, I find that a system where the human-machine interface is very > visual is better. >
At the same time, I think we should keep the simple metamath substitution algorithm because a beginner will understand that. The other systems are much more complicated and difficult to understand. Something like nat.mm would finally be fine if we could make a provisios system simpler than the $d statements. -- FL -- 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/cce2e19a-2ab1-41a2-ba54-adf0a352b202%40googlegroups.com.
