You can update my mathbox. However, this is clearly a maintenance edit, and in principle no permission is needed per http://us.metamath.org/mpeuni/mathbox.html: "other people may make maintenance edits to your mathbox for things like keeping it synchronized with the rest of set.mm, reducing proof lengths, moving your theorems to the main part of set.mm when needed, and fixing typos or other errors." I guess we could add to that, "removing redundant disjoint variable conditions" to be explicit.
For maintenance changes like this affecting many mathboxes, it should be sufficient to announce either here or as a GitHub issue that in say a week you will be making the changes if there are no objections, rather than waiting for every mathbox owner to respond. Norm On Wednesday, December 1, 2021 at 2:32:17 AM UTC-5 [email protected] wrote: > Same here. > > -stan > > On Wed, Dec 1, 2021 at 6:44 AM Thierry Arnoux <[email protected]> wrote: > > > > No problem for me either, you can go ahead and update my Mathbox. > > > > > > Le 1 déc. 2021 à 12:34, 'Alexander van der Vekens' via Metamath < > [email protected]> a écrit : > > > > > > It's fine for me if you clean up my mathbox. > > > > Alexander > > > > -- > > 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/08500d13-564b-436f-b955-fbf0b2b684b8n%40googlegroups.com > . > > > > -- > > 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/42E8D556-4355-4A0C-8CEC-344552DE4275%40gmx.net > . > -- 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/d9cd7861-b165-45ba-a42a-87076f3a93e7n%40googlegroups.com.
