Metamath-lamp version 20 <https://expln.github.io/lamp/v20/index.html> supports reordering of variables in DV conditions.
Variables are ordered by type and name. Ordering by type may be customized on the Settings tab by the "Sort disjoint variables by type" setting. It contains space separated list of types in the order which should be used in DV conditions. Omitted types will be placed at the end of DV conditions. By default, it is "class wff". On Thursday, October 19, 2023 at 6:35:10 AM UTC+2 [email protected] wrote: > 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/8d010640-66c4-49df-b71f-d180d2c3dbdbn%40googlegroups.com.
