test and docs for corres method + slight tweaks for the same
#656
Conversation
|
Tagging @Xaphiosis just in case he wants to read through this (but completely fine to ignore) |
lsf37
force-pushed
the
corres-method-test
branch
2 times, most recently
from
428d37d
to
46c52c3
Compare
There was a problem hiding this comment.
Good examples, definitely very helpful. There's some confusion about which commit some changes are in, and I left a bit of feedback on the text in comments along with begging for a review of just frequency. Might also make sense to use sections in the test file, I find it hard to tell in places what is a section header and what isn't.
This is useful for debugging the proof method for solving side conditions, and will show which goals corres_cleanup is invoked on. Signed-off-by: Gerwin Klein <[email protected]>
The subst_all rule in the standard simp set can circumvent the (no_asm) mode of simp, which we are using in the corres method. Signed-off-by: Gerwin Klein <[email protected]>
I re-read the text and I wholeheartedly apologise for the unjust frequency of
Yes, I should probably do that. Will try it out. |
The (no_asm) for corres goals is now properly enforced, which means it is now really necessary to provide terminal corres rules in their proper form. Signed-off-by: Gerwin Klein <[email protected]>
Explain that these are not nice simp rules, what one should do instead, and why we leave them as is despite all that. Signed-off-by: Gerwin Klein <[email protected]>
Factor out is_safe_wp from corres method, so that we can refer to it later in the documentation. Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
lsf37
force-pushed
the
corres-method-test
branch
from
fe5e85d
to
c5c7bc5
Compare
correscorres_cleanupcorresmethod, which also serves as a longer test case