diff --git a/exercises/ex_01_swap.v b/exercises/ex_01_swap.v index 1a51665c53184eebea28207cf73c0a0e3c0fd7b9..64f1da7271878ba65c102473f00ebf90a84130ee 100644 --- a/exercises/ex_01_swap.v +++ b/exercises/ex_01_swap.v @@ -46,7 +46,7 @@ Lemma swap_spec x y v1 v2 : Which is logically equivalent to [ P -∗ WP e {{ x, x = v ∗ Q }} ] In practice, the "Texan triple" is not more difficult to prove, but usually - easier to use other proofs, because the post-condition does not have to + easier to use in other proofs, because the post-condition does not have to syntactically match [Q]. Using this way of stating specifications, the consequence and framing rule is implicitly applied on the post-condition. diff --git a/solutions/ex_01_swap.v b/solutions/ex_01_swap.v index 6a10f86d079ae05760b98b190a5cac6074af0edf..31ded3076de8ade1b065c2471b553d03b6036bb0 100644 --- a/solutions/ex_01_swap.v +++ b/solutions/ex_01_swap.v @@ -46,7 +46,7 @@ Lemma swap_spec x y v1 v2 : Which is logically equivalent to [ P -∗ WP e {{ x, x = v ∗ Q }} ] In practice, the "Texan triple" is not more difficult to prove, but usually - easier to use other proofs, because the post-condition does not have to + easier to use in other proofs, because the post-condition does not have to syntactically match [Q]. Using this way of stating specifications, the consequence and framing rule is implicitly applied on the post-condition.