Okay. Since the consensus seems to be to go ahead, here is the pull request: https://github.com/metamath/set.mm/pull/2339. That's the last one. After that is merged, all of the mm files will be free of dv conditions on unused variables.
On Wednesday, December 1, 2021 at 7:34:56 AM UTC-7 Norman Megill wrote: > > 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/9b1007e1-8bf5-4d8d-ab36-b4d7a8f30f57n%40googlegroups.com.
