week2 tweak

Signed-off-by: Jim Pryor <profjim@jimpryor.net>

diff --git a/week2.mdwn b/week2.mdwn
index eedc6de..bd86cbb 100644 (file)
--- 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 L<sub>1</sub> ... L<sub>n</sub> x y ~~> y
 </code></pre>
 
 N L<sub>1</sub> ... L<sub>n</sub> x y ~~> y
 </code></pre>
 

-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.
 
 
 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.