summaryrefslogtreecommitdiffstats
path: root/site/posts/Ltac101.v
diff options
context:
space:
mode:
authorThomas Letan <lthms@soap.coffee>2020-02-17 22:24:24 +0100
committerThomas Letan <lthms@soap.coffee>2020-02-17 22:24:24 +0100
commit44fc8666ff95de96229e45ae252519d9ad6fe8d5 (patch)
tree30c46a4166c7359e34b2d2614727a34a022e8ec4 /site/posts/Ltac101.v
parent2a48b7a0df3ac4491eb5cc17a8c7ebf5899e0bc9 (diff)
Render inline math at build time using KaTeX
Diffstat (limited to 'site/posts/Ltac101.v')
-rw-r--r--site/posts/Ltac101.v17
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]: *)