summaryrefslogtreecommitdiffstats
path: root/site/posts/Ltac101.v
diff options
context:
space:
mode:
authorThomas Letan <lthms@soap.coffee>2020-02-23 17:23:06 +0100
committerThomas Letan <lthms@soap.coffee>2020-02-23 17:27:19 +0100
commitd5f4ab5e2e84dcf4a0f6f0e5082c0cd461f4961e (patch)
treec83771d569148c67291d6fe36c3d762f50e8a843 /site/posts/Ltac101.v
parent69f9af2bcec19fd7ae13ac07eda258b140917844 (diff)
Fix a typo in “Ltac 101”
Diffstat (limited to 'site/posts/Ltac101.v')
-rw-r--r--site/posts/Ltac101.v3
1 files changed, 1 insertions, 2 deletions
diff --git a/site/posts/Ltac101.v b/site/posts/Ltac101.v
index f71510f..1bc9907 100644
--- a/site/posts/Ltac101.v
+++ b/site/posts/Ltac101.v
@@ -20,8 +20,7 @@
To take a concrete example, the very first tactic I wrote was for a project
called SpecCert where _many_ lemmas are basically about proving a given
property [P] is a state invariant of a given transition system. As a
- consequence, they have the very same “shape:”
-
+ consequence, they have the very same “shape”:
#<span class="imath">#\forall s\ l\ s', P(s) \wedge s \overset{l\ }{\mapsto}
s' \rightarrow P(s')#</span>#, that is, if [P] is satisfied for [s], and there
exists a transition from [s] to [s'], then [P] is satisfied for [s'].