search

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
607 stars 132 forks source link

reorder and rename equantifiers by specifying pattern(s) underneath #1259

Open mn200 opened 5 days ago

mn200 commented 5 days ago

If you don't want to rely on the order of the variables or their names, how do we pull the quantifier block into shape? The names in the pattern can give names to the quantified variables, and then perhaps sort alphabetically to the order.

xrchz commented 4 days ago

maybe with an option to provide an ordering, then a wrapper that picks alphabetical