From 804d759c8bdecebc0d0e57d423916d6572cec5a8 Mon Sep 17 00:00:00 2001 From: Yasuhiko Watanabe Date: Wed, 9 Jan 2019 07:12:00 +0900 Subject: [PATCH] Typo. --- src/plfa/Lambda.lagda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/Lambda.lagda b/src/plfa/Lambda.lagda index 3521ae96..9f6a1621 100644 --- a/src/plfa/Lambda.lagda +++ b/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 `w`, the variable we are substituting for, +* For abstractions, we compare `y`, the variable we are substituting for, with `x`, the variable bound in the abstraction. If they are the same, we yield the abstraction unchanged, otherwise we subsititute inside the body.