From: Jim Pryor <profjim@jimpryor.net>
Date: Sun, 19 Sep 2010 22:47:13 +0000 (-0400)
Subject: week2: ~~>_eta
X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=82558787dab095c164d4a6d2cdfceebc9b335698

week2: ~~>_eta

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

diff --git a/week2.mdwn b/week2.mdwn
index 1e3aa2bc..eedc6de0 100644
--- a/week2.mdwn
+++ b/week2.mdwn
@@ -318,6 +318,8 @@ will eta-reduce by n steps to:
 
 	\x. M
 
+When we add eta-reduction to our proof system, we end up reconstruing the meaning of `~~>` and `<~~>` and "normal form", all in terms that permit eta-reduction as well. Sometimes these expressions will be annotated to indicate whether only beta-reduction is allowed (<code>~~><sub>&beta;</sub></code>) or whether both beta- and eta-reduction is allowed (<code>~~><sub>&beta;&eta;</sub></code>).
+
 The logical system you get when eta-reduction is added to the proof system has the following property:
 
 >	if `M`, `N` are normal forms with no free variables, then <code>M &equiv; N</code> iff `M` and `N` behave the same with respect to every possible sequence of arguments.