**diff options**

author | Thomas Letan <lthms@soap.coffee> | 2020-02-23 17:23:06 +0100 |
---|---|---|

committer | Thomas Letan <lthms@soap.coffee> | 2020-02-23 17:27:19 +0100 |

commit | d5f4ab5e2e84dcf4a0f6f0e5082c0cd461f4961e (patch) | |

tree | c83771d569148c67291d6fe36c3d762f50e8a843 /site/posts/Ltac101.v | |

parent | 69f9af2bcec19fd7ae13ac07eda258b140917844 (diff) |

Fix a typo in “Ltac 101”

Diffstat (limited to 'site/posts/Ltac101.v')

-rw-r--r-- | site/posts/Ltac101.v | 3 |

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']. |