From 04248526baf154bdbc923520963cbe4f0a567958 Mon Sep 17 00:00:00 2001
From: Daniel Patterson <dbp@dbpmail.net>
Date: Fri, 19 Jan 2018 20:14:27 -0500
Subject: [PATCH] Change some styling

---
 css/default.css                               |  9 +++++-
 ...6-how-to-prove-a-compiler-correct.markdown | 30 +++++++++----------
 2 files changed, 23 insertions(+), 16 deletions(-)

diff --git a/css/default.css b/css/default.css
index 81a77bc..6abf217 100644
--- a/css/default.css
+++ b/css/default.css
@@ -160,13 +160,20 @@ tr:nth-child(even){
 }
 
 blockquote {
-    border-left: 7px solid #900;
+    border-left: 10px solid #900;
     padding: 5px;
     padding-left: 10px;
     margin-left: 15px;
     background-color: #efefef;
 }
 
+pre {
+    border-left: 10px solid gray;
+    padding-left: 15px;
+    margin-left: 10px;
+}
+}
+
 blockquote p {
     padding: 0;
     margin: 0;
diff --git a/essays/2018-01-16-how-to-prove-a-compiler-correct.markdown b/essays/2018-01-16-how-to-prove-a-compiler-correct.markdown
index 7498052..228b98a 100644
--- a/essays/2018-01-16-how-to-prove-a-compiler-correct.markdown
+++ b/essays/2018-01-16-how-to-prove-a-compiler-correct.markdown
@@ -250,11 +250,11 @@ induction a; intros; simpl; iauto.
 We now end up with _better_ inductive hypotheses:
 
 ```
-  IHa1 : forall xs : list StackOp, eval nil (compile a1 ++ xs) = eval (eval' a1 :: nil) xs
-  IHa2 : forall xs : list StackOp, eval nil (compile a2 ++ xs) = eval (eval' a2 :: nil) xs
-  ============================
-  eval nil ((compile a1 ++ compile a2 ++ SPlus :: nil) ++ xs) =
-  eval ((eval' a1 + eval' a2)%Z :: nil) xs
+IHa1 : forall xs : list StackOp, eval nil (compile a1 ++ xs) = eval (eval' a1 :: nil) xs
+IHa2 : forall xs : list StackOp, eval nil (compile a2 ++ xs) = eval (eval' a2 :: nil) xs
+============================
+eval nil ((compile a1 ++ compile a2 ++ SPlus :: nil) ++ xs) =
+eval ((eval' a1 + eval' a2)%Z :: nil) xs
 ```
 
 We need to reshuffle the list associativity and then we can rewrite using the first hypotheses:
@@ -270,11 +270,11 @@ the same). The issue is that `IHa2` needs the stack to be empty, and the stack
 we now have (since we used `IHa1`) is `eval' a1 :: nil`, so it can't be used:
 
 ```
-  IHa1 : forall xs : list StackOp, eval nil (compile a1 ++ xs) = eval (eval' a1 :: nil) xs
-  IHa2 : forall xs : list StackOp, eval nil (compile a2 ++ xs) = eval (eval' a2 :: nil) xs
-  ============================
-  eval (eval' a1 :: nil) ((compile a2 ++ SPlus :: nil) ++ xs) =
-  eval ((eval' a1 + eval' a2)%Z :: nil) xs
+IHa1 : forall xs : list StackOp, eval nil (compile a1 ++ xs) = eval (eval' a1 :: nil) xs
+IHa2 : forall xs : list StackOp, eval nil (compile a2 ++ xs) = eval (eval' a2 :: nil) xs
+============================
+eval (eval' a1 :: nil) ((compile a2 ++ SPlus :: nil) ++ xs) =
+eval ((eval' a1 + eval' a2)%Z :: nil) xs
 ```
 
 The solution is to go back to what our Lemma statement said and generalize it
@@ -295,11 +295,11 @@ induction a; intros; simpl; iauto.
 We run into an odd problem. We have a silly obligation:
 
 ```
-  match s with
-  | nil => eval (i :: s) xs
-  | (_ :: nil)%list => eval (i :: s) xs
-  | (_ :: _ :: _)%list => eval (i :: s) xs
-  end = eval (i :: s) xs
+match s with
+| nil => eval (i :: s) xs
+| (_ :: nil)%list => eval (i :: s) xs
+| (_ :: _ :: _)%list => eval (i :: s) xs
+end = eval (i :: s) xs
 ```
 
 Which will go away once we break apart the list `s` and simplify (if you look