> What I am more interested in is what you guys think a proof assistant SHOULD > do.
Any of the proposals in your message sound fine to me. The mmj2 system doesn't seem to constrain the way we can name things in set.mm enough to seem like a problem to me, but some of the other options seem also aesthetically pleasing enough and a bit more elegant in terms of avoiding the potential for name conflicts. -- 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 visit https://groups.google.com/d/msgid/metamath/B2AB1E33-5B24-4B67-97E0-64C1C0DCFDD0%40panix.com.
