My earliest additions to my mathbox date back to 09-2013. If I remember
right, I was the first using a personal prefix in his mathbox. The
motivation then was to avoid name clashes. This turned out later to be
quite useful, if not necessary, because I keep duplicates like wl-imim2
based on a different set of axioms than the main part.
In the past 6 years nobody objected to this practice, and when occasionally
theorems found their way to the main part, removing the prefix was never an
issue.
I don't see why people should not have the freedom to use their own naming
scheme for whatever reason in their mathbox. This provides even a chance to
suggest an improvement over the main part.
So unless a general renaming to something convincing is in progress, I am
not inclined to 'fix' my personal mathbox.
Wolf
Am Freitag, 27. Dezember 2019 23:23:37 UTC+1 schrieb Benoit:
>
> 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/8803417f-fd20-41ae-b7ee-8357db8f3242%40googlegroups.com.
