summaryrefslogtreecommitdiffstats
path: root/site/posts/RewritingInCoq.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/RewritingInCoq.v
parent3deedaa389ab67148e1ca55febf919b30fbb4df2 (diff)
Prepare the introduction of a RSS feed
Diffstat (limited to 'site/posts/RewritingInCoq.v')
-rw-r--r--site/posts/RewritingInCoq.v24
1 files changed, 10 insertions, 14 deletions
diff --git a/site/posts/RewritingInCoq.v b/site/posts/RewritingInCoq.v
index 9c2efaf..0020a3e 100644
--- a/site/posts/RewritingInCoq.v
+++ b/site/posts/RewritingInCoq.v
@@ -1,17 +1,13 @@
-(** * Rewriting in Coq
-
- This article has originally been published on #<span class="time">May 13,
- 2017</span>.# *)
-
-(** I have to confess something. In the published codebase of SpecCert lies a
- shameful secret. It takes the form of a set of axioms which are not
- required. I thought they were when I wrote them, but it was before I heard
- about “generalized rewriting,” setoids and morphisms.
-
- Now, I know the truth. I will have to update SpecCert eventually. But,
- in the meantime, let me try to explain how it is possible to rewrite a
- term in a proof using a ad-hoc equivalence relation and, when
- necessary, a proper morphism. *)
+(** * Rewriting in Coq *)
+
+(** I have to confess something. In the codebase of SpecCert lies a shameful
+ secret. It takes the form of a set of unnecessary axioms. I thought I
+ couldn’t avoid them at first, but it was before I heard about “generalized
+ rewriting,” setoids and morphisms. Now, I know the truth, and I will have
+ to update SpecCert eventually. But, in the meantime, let me try to explain
+ in this article originally published on #<span id="original-created-at">May
+ 13, 2017</span> how it is possible to rewrite a term in a proof using a
+ ad-hoc equivalence relation and, when necessary, a proper morphism. *)
(** #<div id="generate-toc"></div>#