summaryrefslogtreecommitdiffstats
path: root/site/posts/StronglySpecifiedFunctionsProgram.v
diff options
context:
space:
mode:
authorThomas Letan <lthms@soap.coffee>2020-02-16 22:35:11 +0100
committerThomas Letan <lthms@soap.coffee>2020-02-16 22:35:11 +0100
commitb47ee36ceab517ba84234bf09e3bb01035450a9a (patch)
tree9d5cad60ba02a7a724f3c660f3b91e781bf0676d /site/posts/StronglySpecifiedFunctionsProgram.v
parent25e6a8c049dbc19ac752dda5995929695a1e10f1 (diff)
Automatically generate a revision table from git history
Diffstat (limited to 'site/posts/StronglySpecifiedFunctionsProgram.v')
-rw-r--r--site/posts/StronglySpecifiedFunctionsProgram.v19
1 files changed, 7 insertions, 12 deletions
diff --git a/site/posts/StronglySpecifiedFunctionsProgram.v b/site/posts/StronglySpecifiedFunctionsProgram.v
index 24faf27..037b0dd 100644
--- a/site/posts/StronglySpecifiedFunctionsProgram.v
+++ b/site/posts/StronglySpecifiedFunctionsProgram.v
@@ -1,18 +1,13 @@
-(** #
-<h1>Strongly-Specified Functions in Coq, part 2: the <code>Program</code> Framework</h1>
+(** #<h1>Strongly-Specified Functions in Coq, part 2: the <code>Program</code> Framework</h1>#
-<p>
- This is the second article (initially published on <span class="time">January
- 01, 2017</span>) of a series of two on how to write strongly-specified
- functions in Coq. You can read the previous part <a
- href="/posts/StronglySpecifiedFunctions">here</a>.
-</p>
-# *)
+ This is the second article (initially published on #<span
+ class="time">January 01, 2017</span>#) of a series of two on how to write
+ strongly-specified functions in Coq. You can read the previous part #<a
+ href="/posts/StronglySpecifiedFunctions">here</a>#. # *)
-(** #<div id="generate-toc"></div># *)
+(** #<div id="generate-toc"></div>#
-(** For the past few weeks, I have been playing around with the <<Program>> (or
- Russel) framework of Coq. *)
+ #<div id="history">site/posts/StronglySpecifiedFunctionsProgram.v</div># *)
(** ** The Theory *)