Merge branch 'dev' into pr2

Makefile

@@ -1,5 +1,5 @@
-agda := $(shell find src tspl -type f -name '*.lagda')
-agdai := $(shell find src tspl -type f -name '*.agdai')
+agda := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/tspl/*' \) -and -name '*.lagda')
+agdai := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/tspl/*' \) -and -name '*.agdai')
 markdown := $(subst tspl/,out/,$(subst src/,out/,$(subst .lagda,.md,$(agda))))
 PLFA_DIR := $(shell dirname $(realpath $(lastword $(MAKEFILE_LIST))))
 AGDA2HTML_FLAGS := --verbose --link-to-local-agda-names --use-jekyll=out/
@@ -84,6 +84,13 @@ clobber: clean
 .phony: clobber
 
 
+# List all .lagda files
+ls:
+	@echo $(agda)
+
+.phony: ls
+
+
 # MacOS Setup (install Bundler)
 macos-setup:
 	brew install libxml2

src/plfa/Lambda.lagda

@@ -464,7 +464,7 @@ Let's unpack the first three cases:
 with `x`, the variable in the term. If they are the same,
 we yield `V`, otherwise we yield `x` unchanged.
 
-* For abstractions, we compare `y`, the variable we are substituting for,
+* For abstractions, we compare `y`, the substituted variable,
 with `x`, the variable bound in the abstraction. If they are the same,
 we yield the abstraction unchanged, otherwise we subsititute inside the body.
 
@@ -531,14 +531,14 @@ In an informal presentation of the operational semantics,
 the rules for reduction of applications are written as follows:
 
     L —→ L′
-    -------------- ξ-·₁
+    --------------- ξ-·₁
     L · M —→ L′ · M
 
     M —→ M′
     -------------- ξ-·₂
     V · M —→ V · M′
 
-    ---------------------------- β-ƛ
+    ----------------------------- β-ƛ
     (ƛ x ⇒ N) · V —→ N [ x := V ] 
 
 The Agda version of the rules below will be similar, except that universal

src/plfa/Naturals.lagda

@@ -434,8 +434,9 @@ _*_ : ℕ → ℕ → ℕ
 zero  * n  =  zero
 suc m * n  =  n + (m * n)
 \end{code}
+Computing `m * n` returns the sum of `m` copies of `n`.
 
-Again, rewriting gives us two familiar equations:
+Again, rewriting turns the definition into two familiar equations:
 
     0       * n  ≡  0
     (1 + m) * n  ≡  n + (m * n)