Commit 373c84a5 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix typo.

parent 8fda5e97
Pipeline #16658 passed with stage
in 2 minutes and 46 seconds
...@@ -46,7 +46,7 @@ Lemma swap_spec x y v1 v2 : ...@@ -46,7 +46,7 @@ Lemma swap_spec x y v1 v2 :
Which is logically equivalent to [ P -∗ WP e {{ x, x = v ∗ Q }} ] 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 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 syntactically match [Q]. Using this way of stating specifications, the
consequence and framing rule is implicitly applied on the post-condition. consequence and framing rule is implicitly applied on the post-condition.
......
...@@ -46,7 +46,7 @@ Lemma swap_spec x y v1 v2 : ...@@ -46,7 +46,7 @@ Lemma swap_spec x y v1 v2 :
Which is logically equivalent to [ P -∗ WP e {{ x, x = v ∗ Q }} ] 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 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 syntactically match [Q]. Using this way of stating specifications, the
consequence and framing rule is implicitly applied on the post-condition. consequence and framing rule is implicitly applied on the post-condition.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment