From 8ffc49e92992a5e563944a30fe476ba265f70406 Mon Sep 17 00:00:00 2001 From: Jeremy Siek Date: Sun, 29 Mar 2020 16:53:38 -0400 Subject: [PATCH] minor text edit --- src/plfa/part2/Untyped.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part2/Untyped.lagda.md b/src/plfa/part2/Untyped.lagda.md index 28a1f5de..815d88d6 100644 --- a/src/plfa/part2/Untyped.lagda.md +++ b/src/plfa/part2/Untyped.lagda.md @@ -675,7 +675,7 @@ the predecessor of the current argument) and one corresponding to the zero branch of the case. (The cases could be in either order. We put the successor case first to ease comparison with Church numerals.) -Here is the representation of naturals encoded with de Bruijn indexes: +Here is the Scott representation of naturals encoded with de Bruijn indexes: ``` `zero : ∀ {Γ} → (Γ ⊢ ★) `zero = ƛ ƛ (# 0)