diff options
| author | Thomas Letan <lthms@soap.coffee> | 2021-03-28 00:03:41 +0100 |
|---|---|---|
| committer | Thomas Letan <lthms@soap.coffee> | 2021-03-28 14:19:29 +0200 |
| commit | 495f9db0606b0ed09e6fac59dc32de4cdc8c0087 (patch) | |
| tree | 82ea5c5e247c664de247a0f3818f393ffdb00067 /site/posts/Ltac.org | |
| parent | Release of coqffi 1.0.0~beta4 (diff) | |
2021 Spring redesign
Diffstat (limited to 'site/posts/Ltac.org')
| -rw-r--r-- | site/posts/Ltac.org | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/site/posts/Ltac.org b/site/posts/Ltac.org index caba76c..37580cd 100644 --- a/site/posts/Ltac.org +++ b/site/posts/Ltac.org @@ -1,12 +1,16 @@ -#+BEGIN_EXPORT html -<h1>A Series on Ltac</h1> -#+END_EXPORT +#+TITLE: A Series on Ltac + +#+SERIES: ../coq.html +#+SERIES_PREV: ./StronglySpecifiedFunctions.html +#+SERIES_NEXT: ./RewritingInCoq.html Ltac is the “tactic language” of Coq. It is commonly advertised as the common -approach to write proofs, which tends to bias how it is introduced to new Coq -users (/e.g./, in Master courses). In this series, we present Ltac as the -metaprogramming tool it is, since fundamentally it is an imperative language -which allows for constructing Coq terms interactively and incrementally. +approach to write proofs, which tends to bias how it is introduced to +new Coq users[fn::I know /I/ was introduced to Coq in a similar way in +my Master courses.]. In this series, we present Ltac as the +metaprogramming tool it is, since fundamentally it is an imperative +language which allows for constructing Coq terms interactively and +incrementally. - [[./LtacMetaprogramming.html][Ltac is an Imperative Metaprogramming Language]] :: Ltac generates terms, therefore it is a metaprogramming language. It does it |