generated at
2/17/2025, 6:14:43 PM
判定
judgement
型理論
の
判定
x_1:A_1,\cdots,x_n:A_n\vdash t:A
とか
A\; \mathrm{type}
とか
a\in A
と記述する
a
が
項
、
A
が
型