search

expln / metamath-lamp

Metamath-lamp (Lite Assistant for Metamath Proofs) is a GUI-based proof assistant for creating formal mathematical proofs in Metamath that does not require installation (just run it directly using your web browser).
https://expln.github.io/lamp/latest/index.html
MIT License
11 stars 4 forks source link

Reorder variables in DV conditions #172

Closed BTernaryTau closed 8 months ago

BTernaryTau commented 9 months ago

It would be nice if class and wff variables always appeared at the beginning of distinct variable conditions, and if setvars were always in alphabetical order. This would match how mmj2 currently orders variables and help keep set.mm's formatting more consistent.

Currently there isn't an official convention for this, but there is some discussion about creating one (see https://groups.google.com/g/metamath/c/vRXuz7Qs5wY/m/eaxltrMsBwAJ and https://github.com/metamath/set.mm/pull/3573#discussion_r1362383185).

expln commented 9 months ago

This should not be difficult. I will implement this, hopefully in a few days.

expln commented 8 months ago

Reordering of variables in DV conditions is available on dev. 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 in DV conditions. By default, it is "class wff".

expln commented 8 months ago

Reordering of variables in DV conditions is available in version 20.