summaryrefslogtreecommitdiffstats
path: root/site/posts/StronglySpecifiedFunctions.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/StronglySpecifiedFunctions.v
parent25e6a8c049dbc19ac752dda5995929695a1e10f1 (diff)
Automatically generate a revision table from git history
Diffstat (limited to 'site/posts/StronglySpecifiedFunctions.v')
-rw-r--r--site/posts/StronglySpecifiedFunctions.v26
1 files changed, 12 insertions, 14 deletions
diff --git a/site/posts/StronglySpecifiedFunctions.v b/site/posts/StronglySpecifiedFunctions.v
index 6564413..3adfe50 100644
--- a/site/posts/StronglySpecifiedFunctions.v
+++ b/site/posts/StronglySpecifiedFunctions.v
@@ -1,13 +1,9 @@
-(** #
-<h1>Strongly-Specified Functions in Coq, part 1: using the <code>refine</code> Tactic</h1>
+(** # <h1>Strongly-Specified Functions in Coq, part 1: using the <code>refine</code> Tactic</h1>#
-<p>
- 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="/posts/StronglySpecifiedFunctionsProgram">here</a>.
-</p>
-# *)
+ 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="/posts/StronglySpecifiedFunctionsProgram">here</a>#. *)
(** I started to play with Coq, the interactive theorem prover
developed by Inria, a few weeks ago. It is a very powerful tool,
@@ -23,16 +19,18 @@
return value is the list passed in argument in which the first
element has been removed for example.
- But since we will manipulate lists in this article, we first
+ #<div id="generate-toc"></div>#
+
+ #<div id="history">site/posts/StronglySpecifiedFunctions.v</div># *)
+
+(** ** Is this list empty? *)
+
+(** Since we will manipulate lists in this article, we first
enable several notations of the standard library. *)
From Coq Require Import List.
Import ListNotations.
-(** #<div id="generate-toc"></div># *)
-
-(** ** Is this list empty? *)
-
(** It's the first question to deal with when manipulating
lists. There are some functions that require their arguments not
to be empty. It's the case for the [pop] function, for instance: