**diff options**

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

committer | Thomas Letan <lthms@soap.coffee> | 2020-02-17 22:24:24 +0100 |

commit | 44fc8666ff95de96229e45ae252519d9ad6fe8d5 (patch) | |

tree | 30c46a4166c7359e34b2d2614727a34a022e8ec4 /site/posts/Ltac101.v | |

parent | 2a48b7a0df3ac4491eb5cc17a8c7ebf5899e0bc9 (diff) |

Render inline math at build time using KaTeX

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

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

1 files changed, 9 insertions, 8 deletions

diff --git a/site/posts/Ltac101.v b/site/posts/Ltac101.v index 61d3bc9..7b3c02a 100644 --- a/site/posts/Ltac101.v +++ b/site/posts/Ltac101.v @@ -22,17 +22,18 @@ property [P] is a state invariant of a given transition system. As a consequence, they have the very same “shape:” - \( \forall s\ l\ s', P(s) \wedge s \overset{l\ }{\mapsto} s' \rightarrow P(s') \), - that is, if [P] is satisfied for [s], and there exists a transition from [s] - to [s'], then [P] is satisfied for [s']. + #<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']. Both states and labels are encoded in record, and the first thing I was doing at the time with them was [destruct]ing them. Similarly, the predicate - [P] is an aggregation of sub-predicates (using \( \wedge \)). In practice, - most of my proofs started with something like [intros [x1 [y1 z1]] [a b] [x2 - [y2 z2]] [HP1 [HP2 [HP3 HP4]]] [R1|R2]]. Nothing copy/past cannot solve at - first, of course, but as soon as the definitions change, you have to change - every single [intros] and it is quite boring, to say the least. + [P] is an aggregation of sub-predicates (using #<span + class="imath">#\wedge#</span>#). In practice, most of my proofs started with + something like [intros [x1 [y1 z1]] [a b] [x2 [y2 z2]] [HP1 [HP2 [HP3 HP4]]] + [R1|R2]]. Nothing copy/past cannot solve at first, of course, but as soon as + the definitions change, you have to change every single [intros] and it is + quite boring, to say the least. The solution is simple: define a new tactic to use in place of your “raw” [intros]: *) |