I've filed a feature request for metamath-lamp to follow mmj2's behavior: https://github.com/expln/metamath-lamp/issues/172
On Wednesday, October 18, 2023 at 2:21:42 AM UTC-4 [email protected] wrote: > IMO class/wff variables should come at the beginning, with the list of > setvars being read as a (non)dependency specification for the class/wff > variable. I most recently visited this question for mm-web-rs, which does > not put the class/wff variables first - it just sorts all the variables, > meaning classes come first but "ph" comes between "p" and "q" - because you > need to be set.mm specific to treat class/wff variables differently from > other variables. This is likely to be a problem for other metamath > processors which try not to be set.mm specific, unless we introduce a new > $j command or interpret an existing one as a way to say that setvars come > after other things. > > But also, this is not a thing that users should ever have to think about. > It should be implemented in the set.mm formatter so that even if an > authoring tool comes up with a weird order it is automatically normalized. > (But tools should also strive to honor the default convention because it's > best if the formatter doesn't need to do anything.) > > On Wed, Oct 18, 2023 at 2:09 AM 'Alexander van der Vekens' via Metamath < > [email protected]> wrote: > >> $d statements (disjoint variable restrictions) can contain two or more >> variables (wff, setvar and class variables). The order of them is >> arbitrary, but it could be helpful to have conventions how they should be >> ordered. These conventions should be also implemented in the tools which >> create $d-statements. >> >> Until now, it seems that there are the (unwritten) conventions that class >> variables and wff variables should be at the beginning or the end, and that >> setvar variables are alphabetically ordered. >> >> * In the Metamath book and >> https://us.metamath.org/mpeuni/mmset.html#distinct, class variables and >> wwf variables are always at the end. >> * mmj2 creates d$ statements with class variables and wwf variables at >> the beginning. >> * the html pages for the theorems display class variables and wwf >> variables at the beginning. >> >> mm-lamp, however, seems to create $d statements in arbitrary order (at >> least it puts class variables in the middle, see ~ cplgredgex, and does not >> always order the setvar variables alphabetically). >> >> In my opinion, we should fix the conventions (in section "Conventions" in >> set.mm) that: >> * each $d statement should contain at most one class or wff variable >> * the class variable and the wff variable should be at the beginning or >> the end >> * that setvar variables should be alphabetically ordered >> >> The tools should respect these conventions. >> >> -- >> 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/a976c123-c431-4ec8-a3a2-f14c5ff88527n%40googlegroups.com >> >> <https://groups.google.com/d/msgid/metamath/a976c123-c431-4ec8-a3a2-f14c5ff88527n%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> > -- 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/3dd54288-d3a2-41b6-ab7f-4a49be29bb65n%40googlegroups.com.
