fixed suc_

src/plfa/part2/Untyped.lagda.md

@@ -681,7 +681,7 @@ Here is the representation of naturals encoded with de Bruijn indexes:
 `zero = ƛ ƛ (# 0)
 
 `suc_ : ∀ {Γ} → (Γ ⊢ ★) → (Γ ⊢ ★)
-`suc_ M  = (ƛ ƛ ƛ (# 1 · # 2)) · M
+`suc_ M  = (ƛ ƛ ƛ (# 1 · (# 2 · # 1 · # 0))) · M
 
 case : ∀ {Γ} → (Γ ⊢ ★) → (Γ ⊢ ★) → (Γ , ★ ⊢ ★)  → (Γ ⊢ ★)
 case L M N = L · (ƛ N) · M
@@ -691,6 +691,24 @@ definitions.  The successor branch expects an additional variable to
 be in scope (as indicated by its type), so it is converted to an
 ordinary term using lambda abstraction.
 
+Applying successor to the zero indeed reduces to the Church numeral
+for one.
+
+```
+_ : eval (gas 100) (`suc_ {∅} `zero) ≡
+    steps
+        ((ƛ (ƛ (ƛ (` (S Z)) · ((` (S (S Z))) · (` (S Z)) · (` Z))))) · (ƛ (ƛ (` Z)))
+      —→⟨ β ⟩
+        ƛ (ƛ (` (S Z)) · ((ƛ (ƛ (` Z))) · (` (S Z)) · (` Z)))
+      —→⟨ ζ (ζ (ξ₂ (ξ₁ β))) ⟩
+        ƛ (ƛ (` (S Z)) · ((ƛ (` Z)) · (` Z)))
+      —→⟨ ζ (ζ (ξ₂ β)) ⟩
+        ƛ (ƛ (` (S Z)) · (` Z))
+      ∎)
+    (done (ƛ (ƛ (′ (` (S Z)) · (′ (` Z))))))
+_ = refl
+```
+
 We can also define fixpoint.  Using named terms, we define:
 
     μ f = (ƛ x ⇒ f · (x · x)) · (ƛ x ⇒ f · (x · x))
@@ -729,6 +747,7 @@ Because `` `suc `` is now a defined term rather than primitive,
 it is no longer the case that `plus · two · two` reduces to `four`,
 but they do both reduce to the same normal term.
 
+
 #### Exercise `plus-eval` (practice)
 
 Use the evaluator to confirm that `plus · two · two` and `four`