Bdep #603
Draft
Bdep #603
Conversation
This file contains 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
…rily) in lospec_test
Merge before push
This family of functions type-check a formula w.r.t. a memory that is infered from the program logic goal. The commit changes two things: - for prhl, its uses the same memory name as the one used in the program logic goal. (Previously, it was using `mhr`) - its returns the memory that has been used for the type-checking
- EcMatching.Zipper.map
- EcLowPhlGoal.{is_program_logic,hl_set_stmt}
This tactic allows to change an expression in a statement by some
other expression. When applied, the user has to prove that the two
expressions are equal (generalizing over all the program variables)
This tactic applies to any program logic.
The syntax is:
proc change <side?> <codepos> : <form>
This tactic is in the TCB.
Test plan:
- unit test (tests/prochange.ec)
This tactic allows to rewrite an expression in a statement.
The syntax is:
proc rewrite <side?> <codepos> <proof-term>
This tactic does not aim to be in the TCB and its final
version should rely on "proc change".
Test plan:
- unit test (tests/procrewrite.ec)
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.
No description provided.