Hi all, I found it convenient to label most of the theorems in my mathbox as bj-xxx (my initials). This allows me to do things like "MM> verify proof bj-*" and other things like bulk minimizations and potentially more things. I find it convenient to have a "namespace" to do these kinds of things. I can also notice more easily when one of these theorems is used in a proof. Obviously, when/if they go to the main part, the prefix should be removed. Actually, if other mathboxes had this convention, it would be easier for us to spot when we're using a theorem from another mathbox and then to move it to the main part, or at least to duplicate it.
David recently remarked (https://groups.google.com/d/msg/metamath/OyBTnESDvnM/rFCBvqJcCwAJ) that this convention may make it harder to move theorems to the main part: one would need to relabel them, maybe with some complications coming from label clashes. I do not think this outweighs the above benefits, but I may be missing some other implications. What do you think ? Also, I would like to find a way to foster collaborations between mathboxes. For the moment, MM does not look at other mathboxes when doing MM> IMPROVE, MINIMIZE, or similar things (although there is an option /include mathboxes). I do not know about mmj2, but it uses at most mathboxes which are before ours. Could there be a method, a script or anything that, when a contributor starts proving stuff, it automatically positions his mathbox last, and signals when theorems from other mathboxes are used (and at the end of the session, restores the original order of the mathboxes) ? This might be doable with the /SPLIT option introduced recently by Norm. Benoît -- 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/32b5e202-8291-437e-b4d8-f0e41629ef6a%40googlegroups.com.
