From 495f9db0606b0ed09e6fac59dc32de4cdc8c0087 Mon Sep 17 00:00:00 2001
From: Thomas Letan <lthms@soap.coffee>
Date: Sun, 28 Mar 2021 00:03:41 +0100
Subject: 2021 Spring redesign

---
 site/posts/StronglySpecifiedFunctionsRefine.v | 20 +++++++++++++-------
 1 file changed, 13 insertions(+), 7 deletions(-)

(limited to 'site/posts/StronglySpecifiedFunctionsRefine.v')

diff --git a/site/posts/StronglySpecifiedFunctionsRefine.v b/site/posts/StronglySpecifiedFunctionsRefine.v
index 1d4ec2e..4ffb385 100644
--- a/site/posts/StronglySpecifiedFunctionsRefine.v
+++ b/site/posts/StronglySpecifiedFunctionsRefine.v
@@ -19,7 +19,7 @@
     return value is the list passed in argument in which the first
     element has been removed for example.
 
-    #<div id="generate-toc"></div>#
+    #<nav id="generate-toc"></nav>#
 
     #<div id="history">site/posts/StronglySpecifiedFunctionsRefine.v</div># *)
 
@@ -54,7 +54,8 @@ Import ListNotations.
 <<
 Definition predicate_b (args) :=
   if predicate_dec args then true else false.
->> *)
+>>
+    *)
 
 (** *** Defining the <<empty>> predicate *)
 
@@ -174,7 +175,8 @@ Definition pop {a} (l : list a) (h : ~ empty l)
   h : ~ empty l
   ============================
   list a
->> *)
+>>
+    *)
 
 (** Using the [refine] tactic naively, for instance this way:  *)
 
@@ -280,7 +282,8 @@ Definition pop {a} (l : list a | ~ empty l)
   equ : proj1_sig l = []
   ============================
   {l' : list a | exists a0 : a, proj1_sig l = a0 :: l'}
->> *)
+>>
+    *)
 
   + destruct l as [l nempty]; cbn in *.
     rewrite equ in nempty.
@@ -299,7 +302,8 @@ Definition pop {a} (l : list a | ~ empty l)
   equ : proj1_sig l = a0 :: rst
   ============================
   exists a1 : a, proj1_sig l = a1 :: rst
->> *)
+>>
+    *)
 
   + destruct l as [l nempty]; cbn in *.
     rewrite equ.
@@ -339,7 +343,8 @@ Definition push {a} (l : list a) (x : a)
 <<
 let push l a =
   Cons (a, l)
->> *)
+>>
+    *)
 
 (** ** Defining [head] *)
 
@@ -376,7 +381,8 @@ Defined.
 let head = function
 | Nil -> assert false (* absurd case *)
 | Cons (a, l0) -> a
->> *)
+>>
+    *)
 
 (** ** Conclusion & Moving Forward *)
 
-- 
cgit v1.2.3