(no commit message)

[lambda.git] / topics / _week5_system_F.mdwn

diff --git a/topics/_week5_system_F.mdwn b/topics/_week5_system_F.mdwn
index 684f42b..86f1c75 100644 (file)
--- a/topics/_week5_system_F.mdwn
+++ b/topics/_week5_system_F.mdwn
@@ -18,10 +18,10 @@ System F is due (independently) to Girard and Reynolds.
 It enhances the simply-typed lambda calculus with quantification over
 types.  In System F, you can say things like
 
 It enhances the simply-typed lambda calculus with quantification over
 types.  In System F, you can say things like
 

-<code>&Gamma; &alpha; (\x.x):(&alpha; -> &alpha;)</code>
+<code>&Lambda; &alpha; (\x.x):(&alpha; -> &alpha;)</code>

 
 This says that the identity function maps arguments of type &alpha; to
 
 This says that the identity function maps arguments of type &alpha; to

-results of type &alpha;, for any choice of &alpha;.  So the &Gamma; is
+results of type &alpha;, for any choice of &alpha;.  So the &Lambda; is

 a universal quantifier over types.
 
 
 a universal quantifier over types.