X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2Fweek5_simply_typed.mdwn;h=fc7bfd27731c6f8c7bcf3237bd6415586ab08819;hp=1a0425feef46b5802638cde9bc20e89f57b77490;hb=c04c0731a576ea9e9fcacaf6981e556546ae312d;hpb=340e045ffdf3ebf60771af2d74d0bafe9eb08283 diff --git a/topics/week5_simply_typed.mdwn b/topics/week5_simply_typed.mdwn index 1a0425fe..fc7bfd27 100644 --- a/topics/week5_simply_typed.mdwn +++ b/topics/week5_simply_typed.mdwn @@ -99,8 +99,8 @@ and so on. Given a set of types `T`, we define the set of typed lambda terms Λ_T, which is the smallest set such that -* each type `t` has an infinite set of distinct variables, {x^t}_1, - {x^t}_2, {x^t}_3, ... +* each type `t` has an infinite set of distinct variables, xt1, + xt2, xt3, ... * If a term `M` has type σ -> τ, and a term `N` has type σ, then the application `(M N)` has type τ.