Fixed Agda errors; fixed css errors which resulted in the incorrect font being used.

Makefile

@@ -12,7 +12,7 @@ TMP_DIR := $(CACHE_DIR)/tmp
 #################################################################################
 
 .PHONY: init
-init: setup-check-fix-whitespace setup-check-htmlproofer
+init: setup-check-fix-whitespace setup-install-htmlproofer
 	git config core.hooksPath .githooks
 
 

courses/tspl/2019/Assignment4.lagda.md

@@ -982,9 +982,9 @@ Remember to indent all code by two spaces.
 ```
   ext∋ : ∀ {Γ B x y}
     → x ≢ y
-    → ¬ ∃[ A ]( Γ ∋ x ⦂ A )
+    → ¬ ( ∃[ A ] Γ ∋ x ⦂ A )
       -----------------------------
-    → ¬ ∃[ A ]( Γ , y ⦂ B ∋ x ⦂ A )
+    → ¬ ( ∃[ A ] Γ , y ⦂ B ∋ x ⦂ A )
   ext∋ x≢y _  ⟨ A , Z ⟩       =  x≢y refl
   ext∋ _   ¬∃ ⟨ A , S _ ⊢x ⟩  =  ¬∃ ⟨ A , ⊢x ⟩
 
@@ -1005,8 +1005,8 @@ Remember to indent all code by two spaces.
   ¬arg : ∀ {Γ A B L M}
     → Γ ⊢ L ↑ A ⇒ B
     → ¬ Γ ⊢ M ↓ A
-      -------------------------
-    → ¬ ∃[ B′ ](Γ ⊢ L · M ↑ B′)
+      ----------------------------
+    → ¬ ( ∃[ B′ ] Γ ⊢ L · M ↑ B′ )
   ¬arg ⊢L ¬⊢M ⟨ B′ , ⊢L′ · ⊢M′ ⟩ rewrite dom≡ (uniq-↑ ⊢L ⊢L′) = ¬⊢M ⊢M′
 
   ¬switch : ∀ {Γ M A B}

courses/tspl/2019/Exam.lagda.md

@@ -589,13 +589,14 @@ module Problem3 where
 ```
   ext∋ : ∀ {Γ B x y}
     → x ≢ y
-    → ¬ ∃[ A ]( Γ ∋ x ⦂ A )
+    → ¬ ( ∃[ A ] Γ ∋ x ⦂ A )
       -----------------------------
-    → ¬ ∃[ A ]( Γ , y ⦂ B ∋ x ⦂ A )
+    → ¬ ( ∃[ A ] Γ , y ⦂ B ∋ x ⦂ A )
   ext∋ x≢y _  ⟨ A , Z ⟩       =  x≢y refl
   ext∋ _   ¬∃ ⟨ A , S _ ⊢x ⟩  =  ¬∃ ⟨ A , ⊢x ⟩
 
-  lookup : ∀ (Γ : Context) (x : Id)
+  lookup :
+      ∀ (Γ : Context) (x : Id)
       -----------------------
     → Dec (∃[ A ](Γ ∋ x ⦂ A))
   lookup ∅ x                        =  no  (λ ())
@@ -612,8 +613,8 @@ module Problem3 where
   ¬arg : ∀ {Γ A B L M}
     → Γ ⊢ L ↑ A ⇒ B
     → ¬ Γ ⊢ M ↓ A
-      -------------------------
-    → ¬ ∃[ B′ ](Γ ⊢ L · M ↑ B′)
+      ----------------------------
+    → ¬ ( ∃[ B′ ] Γ ⊢ L · M ↑ B′ )
   ¬arg ⊢L ¬⊢M ⟨ B′ , ⊢L′ · ⊢M′ ⟩ rewrite dom≡ (uniq-↑ ⊢L ⊢L′) = ¬⊢M ⊢M′
 
   ¬switch : ∀ {Γ M A B}

css/minima.scss

@@ -1,5 +1,5 @@
 @import
-    "theme/skins/classic",
-    "theme/initialize",
-    "theme/agda"
+    "minima/skins/classic",
+    "minima/initialize",
+    "minima/agda"
 ;

hs/Main.hs

@@ -336,7 +336,7 @@ main = do
     -- Compile CSS
     match "css/*.css" $ compile compressCssCompiler
 
-    scss <- makePatternDependency "css/theme/**.scss"
+    scss <- makePatternDependency "css/minima/**.scss"
     rulesExtraDependencies [scss] $
       match "css/minima.scss" $
         compile $ sassCompilerWith sassOptions

src/plfa/part2/Inference.lagda.md

@@ -580,9 +580,9 @@ such that `Γ ∋ x ⦂ A` holds, then there is also no type `A` such that
 ```
 ext∋ : ∀ {Γ B x y}
   → x ≢ y
-  → ¬ ∃[ A ]( Γ ∋ x ⦂ A )
+  → ¬ ( ∃[ A ] Γ ∋ x ⦂ A )
     -----------------------------
-  → ¬ ∃[ A ]( Γ , y ⦂ B ∋ x ⦂ A )
+  → ¬ ( ∃[ A ] Γ , y ⦂ B ∋ x ⦂ A )
 ext∋ x≢y _  ⟨ A , Z ⟩       =  x≢y refl
 ext∋ _   ¬∃ ⟨ A , S _ ∋x ⟩  =  ¬∃ ⟨ A , ∋x ⟩
 ```
@@ -638,8 +638,8 @@ there is no term `B′` such that `Γ ⊢ L · M ↑ B′` holds:
 ¬arg : ∀ {Γ A B L M}
   → Γ ⊢ L ↑ A ⇒ B
   → ¬ Γ ⊢ M ↓ A
-    -------------------------
-  → ¬ ∃[ B′ ](Γ ⊢ L · M ↑ B′)
+    ----------------------------
+  → ¬ ( ∃[ B′ ] Γ ⊢ L · M ↑ B′ )
 ¬arg ⊢L ¬⊢M ⟨ B′ , ⊢L′ · ⊢M′ ⟩ rewrite dom≡ (uniq-↑ ⊢L ⊢L′) = ¬⊢M ⊢M′
 ```
 Let `⊢L` be evidence that `Γ ⊢ L ↑ A ⇒ B` holds and `¬⊢M` be evidence