From 0cd3f69b1d8fb7e18a7e0b2bccd86a96d7fd009b Mon Sep 17 00:00:00 2001
From: Matthijs Kooijman <matthijs@stdin.nl>
Date: Tue, 1 Dec 2009 11:12:27 +0100
Subject: [PATCH] =?utf8?q?Add=20note=20about=20=CE=B2-reduction=20for=20ty?=
 =?utf8?q?pe=20variables.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=utf8
Content-Transfer-Encoding: 8bit

---
 Chapters/Normalization.tex | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index 55e0057..cdd57bb 100644
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -812,6 +812,11 @@
         sure that most lambda abstractions will eventually be reducable by
         β-reduction.
 
+        Note that β-reduction also works on type lambda abstractions and type
+        applications as well. This means the substitution below also works on
+        type variables, in the case that the binder is a type variable and teh
+        expression applied to is a type.
+
         \starttrans
         (λx.E) M
         -----------------
@@ -829,6 +834,17 @@
 
         \transexample{beta}{β-reduction}{from}{to}
 
+        \startbuffer[from]
+        (λt.λa::t. a) @Int
+        \stopbuffer
+
+        \startbuffer[to]
+        (λa::Int. a)
+        \stopbuffer
+
+        \transexample{beta-type}{β-reduction for type abstractions}{from}{to}
+
+
       \subsubsection{Empty let removal}
         This transformation is simple: It removes recursive lets that have no bindings
         (which usually occurs when unused let binding removal removes the last
-- 
2.30.2