$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.
