From 56ac5c007eb0623d8cf3512b754f741f9830d7fd Mon Sep 17 00:00:00 2001 From: Philip Wadler Date: Wed, 9 Jan 2019 11:12:23 +0000 Subject: [PATCH] small fixes to Lambda --- src/plfa/Lambda.lagda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/plfa/Lambda.lagda b/src/plfa/Lambda.lagda index 3521ae96..7e350c8d 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 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