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