From c62a61dba7285a034fc0405edbd47dcc48bf03f5 Mon Sep 17 00:00:00 2001 From: Thomas Letan Date: Tue, 14 Jul 2020 11:26:58 +0200 Subject: Prepare the introduction of a RSS feed --- site/posts/RewritingInCoq.v | 24 ++++++++++-------------- 1 file changed, 10 insertions(+), 14 deletions(-) (limited to 'site/posts/RewritingInCoq.v') 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 #May 13, - 2017.# *) - -(** 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 #May + 13, 2017 how it is possible to rewrite a term in a proof using a + ad-hoc equivalence relation and, when necessary, a proper morphism. *) (** #
# -- cgit v1.2.3