From 9d8dfd07484c34af18d22e3a948f76f0c9feb2b3 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Sun, 19 Sep 2010 18:48:27 -0400 Subject: [PATCH] week2 tweak Signed-off-by: Jim Pryor --- week2.mdwn | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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. -- 2.11.0