X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?a=blobdiff_plain;ds=inline;f=topics%2F_week5_system_F.mdwn;h=86f1c75bb9eb48708797946ea766dd58fa96d6b5;hb=c9938f8210260c15fd1a7d5308b3115858e7e9c6;hp=684f42be4087594c9c97768e7f7ef66bcca0bc5b;hpb=e786697f406f29139f4116d13687b37e42594f81;p=lambda.git
diff --git a/topics/_week5_system_F.mdwn b/topics/_week5_system_F.mdwn
index 684f42be..86f1c75b 100644
--- 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
-Γ α (\x.x):(α -> α)
+Λ α (\x.x):(α -> α)
This says that the identity function maps arguments of type α to
-results of type α, for any choice of α. So the Γ is
+results of type α, for any choice of α. So the Λ is
a universal quantifier over types.