ラムダ抽象の型付け規則T-Abs
図自体は簡単なんだけど、各記号の結合の強さが度々わからなくなる
図に括弧が入ることはないので
↑の色は適当
型環境\Gammaが「
変数:型 」の集合であることを強く意識したら理解の助けになる
もっとわかりやすく言うと、\Gammaに単体の「変数」や「型」のみでは含まれないということ
\frac{\Gamma,x: t_1\vdash e:t_2}{\Gamma\vdash\lambda x.e:t_1\to t_2} で良くね？
上の図の下段の
x:T_1のところいらんやろ
