Assumptions are currently not taken into account when checking that a subproof has succeeded in proving its goal at the top-level.
Example:
assume(C)
val ab = have(A |- B)
have(A |- B) subproof {
have(thesis) by Restate.from(ab)
}
Will raise an error saying the subproof proved C; A |- B, instead of the expected sequent A |- B. So, C is being propagated into the subproof as expected, but the top-level correctness check fails to take this assumption into account.
This has been fixed by adding assumptions into the sequent the subproof uses for checking.
Assumptions are currently not taken into account when checking that a subproof has succeeded in proving its goal at the top-level.
Example:
Will raise an error saying the subproof proved
C; A |- B
, instead of the expected sequentA |- B
. So,C
is being propagated into the subproof as expected, but the top-level correctness check fails to take this assumption into account.This has been fixed by adding assumptions into the sequent the subproof uses for checking.