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
626 stars 143 forks source link

rename EVERY2 to LIST_REL in theorem names #316

Open xrchz opened 8 years ago

xrchz commented 8 years ago

EVERY2 and LIST_REL are the same constant (one is an overload for the other). But several theorems use "EVERY2" in their name, which makes it hard to find theorems about "LIST_REL" if one only knows the constant by that name. It would be nice if all the theorems used "LIST_REL" in their name. (Suggested by @SOwens.)

--- Want to back this issue? **[Post a bounty on it!](https://www.bountysource.com/issues/28163666-rename-every2-to-list_rel?utm_campaign=plugin&utm_content=tracker%2F495335&utm_medium=issues&utm_source=github)** We accept bounties via [Bountysource](https://www.bountysource.com/?utm_campaign=plugin&utm_content=tracker%2F495335&utm_medium=issues&utm_source=github).
konrad-slind commented 8 years ago

This is a general problem. If existing constants are going to be renamed/overloaded, then perhaps the search facilities should look at the overloading maps in order to get all the info.

Konrad.

On Wed, Nov 11, 2015 at 11:05 AM, Ramana Kumar notifications@github.com wrote:

EVERY2 and LIST_REL are the same constant (one is an overload for the other). But several theorems use "EVERY2" in their name, which makes it hard to find theorems about "LIST_REL" if one only knows the constant by that name. It would be nice if all the theorems used "LIST_REL" in their name. (Suggested by @SOwens https://github.com/SOwens.)

— Reply to this email directly or view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/316.

mn200 commented 8 years ago

If you want to add additional bindings so that theorems are available under two names, that's fine. On the other hand, don't remove existing bindings to break stuff gratuitously.

I'd tend to use DB.match in preference to DB.find, and then the name of the theorem doesn't really matter.

xrchz commented 7 years ago

319 is relevant

xrchz commented 7 years ago

98 also