From 1d2068e4ad6a692b62da13e2eb94e2b22aa4b3c7 Mon Sep 17 00:00:00 2001
From: wadler <wadler@inf.ed.ac.uk>
Date: Tue, 3 Jul 2018 10:39:03 -0300
Subject: [PATCH] minor fixes

---
 src/plta/Connectives.lagda | 16 ++++++++--------
 src/plta/Lambda.lagda      |  6 +++---
 src/plta/Properties.lagda  |  2 +-
 3 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/src/plta/Connectives.lagda b/src/plta/Connectives.lagda
index 73130cbd..5b45d5a3 100644
--- a/src/plta/Connectives.lagda
+++ b/src/plta/Connectives.lagda
@@ -8,15 +8,15 @@ permalink : /Connectives/
 module plta.Connectives where
 \end{code}
 
-This chapter introduces the basic logical connectives, by observing
-a correspondence between connectives of logic and data types,
-a principle known as *Propositions as Types*.
+This chapter introduces the basic logical connectives, by observing a
+correspondence between connectives of logic and data types, a
+principle known as _Propositions as Types_.
 
-+ *conjunction* is *product*
-+ *disjunction* is *sum*
-+ *true* is *unit type*
-+ *false* is *empty type*
-+ *implication* is *function space*
+  * _conjunction_ is _product_
+  * _disjunction_ is _sum_
+  * _true_ is _unit type_
+  * _false_ is _empty type_
+  * _implication_ is _function space_
 
 
 ## Imports
diff --git a/src/plta/Lambda.lagda b/src/plta/Lambda.lagda
index 51fb2dc7..b6c90214 100644
--- a/src/plta/Lambda.lagda
+++ b/src/plta/Lambda.lagda
@@ -4,18 +4,18 @@ layout    : page
 permalink : /Lambda/
 ---
 
-*Add a couple of simpler examples* ``id · `zero`` and ``twoᶜ · sucᶜ · `zero``.
-
-*Experiment with defining variables* smart constructor `` ƛ`_⇒_ ``
+*Todo: Experiment with defining variable names* smart constructor `` ƛ`_⇒_ ``
 
 \begin{code}
 module plta.Lambda where
 \end{code}
 
+<!--
 [This chapter was originally based on Chapter _Stlc_
 of _Software Foundations_ (_Programming Language Foundations_).
 It has now been updated, but if you spot any plagiarism
 please let me know. – P]
+-->
 
 The _lambda-calculus_, first published by the logician Alonzo Church in
 1932, is a core calculus with only three syntactic constructs:
diff --git a/src/plta/Properties.lagda b/src/plta/Properties.lagda
index fd35c10e..cf889d69 100644
--- a/src/plta/Properties.lagda
+++ b/src/plta/Properties.lagda
@@ -1369,7 +1369,7 @@ det β-zero        β-zero            =  refl
 det (β-suc VL)    (ξ-case L—→L″)    =  ⊥-elim (V¬—→ (V-suc VL) L—→L″)
 det (β-suc _)     (β-suc _)         =  refl
 det β-μ           β-μ               =  refl
--- \end{code}
+\end{code}
 The proof is by induction over possible reductions.  We consider
 three typical cases.