diff options
| author | Thomas Letan <lthms@soap.coffee> | 2020-07-31 09:18:47 +0200 |
|---|---|---|
| committer | Thomas Letan <lthms@soap.coffee> | 2020-07-31 09:18:47 +0200 |
| commit | c2bb9b043bee85e390f4c59d52cb97a489faf85d (patch) | |
| tree | 6ce16f196359980cb820605c0042b3377d876f54 /site/posts/Ltac101.v | |
| parent | “For Fun and Benefit” was not an idiomatic expression (diff) | |
Make the two articles about Ltac refer to each other
Diffstat (limited to 'site/posts/Ltac101.v')
| -rw-r--r-- | site/posts/Ltac101.v | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/site/posts/Ltac101.v b/site/posts/Ltac101.v index b0841e9..2b71a8f 100644 --- a/site/posts/Ltac101.v +++ b/site/posts/Ltac101.v @@ -1,10 +1,14 @@ (** * Ltac 101 *) -(** In this article (originally published on #<span - id="original-created-at">October 16, 2017</span>#), I give an overview of my - findings about the Ltac language, more precisely how it can be used to - automate the construction of proof terms. If you never wrote a tactic in Coq - and are curious about the subject, it might be a good starting point. *) +(** We give an overview of my findings about the Ltac language, more + precisely how it can be used to automate the construction of proof terms. If + you never wrote a tactic in Coq and are curious about the subject, it might + be a good starting point. + + This write-up (originally published on #<span + id="original-created-at">October 16, 2017</span>#) is the first part of a + series on Ltac. The next part explains #<a + href="/posts/MixingLtacAndGallina.html">how to mix Gallina and Ltac</a>#. *) (** #<div id="generate-toc"></div># |