From 373c84a5a8db69c28e8bf2a2ce11bf8074d78623 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Sun, 12 May 2019 22:46:37 +0200 Subject: [PATCH] Fix typo. --- exercises/ex_01_swap.v | 2 +- solutions/ex_01_swap.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/exercises/ex_01_swap.v b/exercises/ex_01_swap.v index 1a51665..64f1da7 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 6a10f86..31ded30 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. -- GitLab