判定
judgement
型理論
の
判定
$ x_1:A_1,\cdots,x_n:A_n\vdash t:A
とか
$ A\; \mathrm{type}
とか
$ a\in A
と記述する
$ a
が
項
、
$ A
が
型