summaryrefslogtreecommitdiffstats
path: root/site/posts/StronglySpecifiedFunctions.v
diff options
context:
space:
mode:
authorThomas Letan <lthms@soap.coffee>2020-07-14 11:26:58 +0200
committerThomas Letan <lthms@soap.coffee>2020-07-14 11:26:58 +0200
commitc62a61dba7285a034fc0405edbd47dcc48bf03f5 (patch)
tree994a21ae6741acb026e73a8d0e85933f04562732 /site/posts/StronglySpecifiedFunctions.v
parent3deedaa389ab67148e1ca55febf919b30fbb4df2 (diff)
Prepare the introduction of a RSS feed
Diffstat (limited to 'site/posts/StronglySpecifiedFunctions.v')
-rw-r--r--site/posts/StronglySpecifiedFunctions.v12
1 files changed, 6 insertions, 6 deletions
diff --git a/site/posts/StronglySpecifiedFunctions.v b/site/posts/StronglySpecifiedFunctions.v
index ac55b7e..5d0e69a 100644
--- a/site/posts/StronglySpecifiedFunctions.v
+++ b/site/posts/StronglySpecifiedFunctions.v
@@ -1,11 +1,11 @@
-(** * Strongly-Specified Functions in Coq, part 1: using the <<refine>> Tactic
+(** * Strongly-Specified Functions in Coq, part 1: using the <<refine>> Tactic *)
- This is the first article (initially published on #<span
- class="time">January 11, 2015</span>#) of a series of two on how to write
- strongly-specified functions in Coq. You can read the next part #<a
- href="./StronglySpecifiedFunctionsProgram.html">here</a>#. *)
+(** This is the first article (initially published on #<span
+ class="original-created-at">January 11, 2015</span>#) of a series of two on
+ how to write strongly-specified functions in Coq. You can read the next part
+ #<a href="./StronglySpecifiedFunctionsProgram.html">here</a>#.
-(** I started to play with Coq, the interactive theorem prover
+ I started to play with Coq, the interactive theorem prover
developed by Inria, a few weeks ago. It is a very powerful tool,
yet hard to master. Fortunately, there are some very good readings
if you want to learn (I recommend the Coq'Art). This article is