Michael Norrish
Michael Norrish
Needs the rewrite that says ``` (?t. !v. v = e ==> P v t) (!v. v = e ==> ?t. P v t) ``` along with a “pair-y” version...
If I include that text in my script file, I do not see a failure. Please be more precise with your "causes it to fail".
An actual test-case would be helpful. The theorems stored with `quotient_simp` are passed to `PURE_REWRITE_RULE` (see the treatment of parameters `tyop_simps` in `src/quotient/src/quotient.sml`) and `PURE_REWRITE_RULE` has no problem interpreting conjunctions...
This .gitignore isn't such a bad idea.
It would be good if you could add a comment above the new material explaining the new constants and how they might be used. If you want to go wild,...
Your PR is failing our source code tests. (Locally, you can replicate this by doing a `build -t`.) In particular, material under `src/` can't use Unicode characters (except for the...
Is this work going to get finished?
Closing as moribund.
This sounds plausible. Notes: 1. The dependency information calculated for graph-purposes is already stored in `.HOLMK/*.d` files that are checked for out-of-date ness; it would be reasonable to extend the...
Do you have to run `Holmake` in a particular mode to get it to ever generate heap files, or do you do that all the time regardless? It seems that...