On 1/4/20 6:59 AM, vvs wrote:
Another reason for confusion might be that there are experienced contributors forgetting about novices learning the craft. The latter want a tutorial database with quite different and simplified conventions and theorems.
That's an interesting suggestion. We could keep debating set.mm conventions for a long time (and I suppose we likely will whether I recommend it or not) but there are a lot of reasons why I don't expect a fundamental rethink of naming in set.mm. Even "sqr" versus "sqrt" which I thought might be low hanging fruit, affects a lot more theorems than I realized before I ran "show label *sqr*" and started looking through the results.
But a tutorial is a different context. There are (well, should be) far fewer theorems. I could even imagine going big and thinking about things like using more illustrations, graphic design which is less information-dense, and any number of things which would be either difficult or undesirable for set.mm itself.
Now, writing tutorials (or textbooks or other teaching material - especially if you want them to be good) is real work so I don't want to deny that. But if someone's creative juices do flow in that direction, it might be a chance to "think outside the set.mm box" to one extent or another.
-- 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/9b57d845-f4b4-dbbb-4791-d069e857b23a%40panix.com.
