343-NotExists.conclude_via_forall() update #344
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Correct some ProofFailure() syntax in logic/booleans/booleans.py where only a string was being used as an argument instead of the now-standard three arguments consisting of an object, current assumptions or other context, and a message string.
Update imports in NotExists().conclude_via_forall() method, plus add two NotExists()-related theorems to help the conclude_via_forall() method work more smoothly by allowing cases where the NotExists() and Forall() objects use conditions vs. no conditions. Also correct an error in constructing a substitution for use in instantiation. Include some testing in the logic/booleans/quantification/existence demonstrations.ipynb notebook.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This updates the
NotExists().conclude_via_forall()method and related code in the following ways:conditionsfrom theNotExists()andForall()objects, which in turn allows instantiations to proceed more smoothly in cases where such conditions do not exist;conclude_via_forall()method, handling separately the cases with conditions vs cases without conditions;ProofError()calls in logic/booleans/booleans.py.The updated code produces no errors during build_alt.py --essential.