From: Jim Pryor Date: Sun, 19 Sep 2010 22:48:27 +0000 (-0400) Subject: week2 tweak X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=9d8dfd07484c34af18d22e3a948f76f0c9feb2b3 week2 tweak Signed-off-by: Jim Pryor --- diff --git a/week2.mdwn b/week2.mdwn index eedc6de0..bd86cbbf 100644 --- a/week2.mdwn +++ b/week2.mdwn @@ -330,7 +330,7 @@ That is, when `M` and `N` are (closed normal forms that are) syntactically disti N L1 ... Ln x y ~~> y -That is, closed normal forms that are not just beta-reduced but also fully eta-reduced, will be syntactically different iff they yield different values for some arguments. That is, iff their extensions differ. +That is, closed beta-plus-eta-normal forms will be syntactically different iff they yield different values for some arguments. That is, iff their extensions differ. So the proof theory with eta-reduction added is called "extensional," because its notion of normal form makes syntactic identity of closed normal forms coincide with extensional equivalence.