113
правок
Изменения
→\lambda\Pi-исчисление
\frac{\Gamma \in \mathrm{WF}}{\Gamma \vdash \mathrm{Type} : \mathrm{Kind}} \text{,} \vspace{3mm} \\
\frac{\Gamma \in \mathrm{WF} \qquad x : T \in \Gamma}{\Gamma \vdash x : T} \text{,} \vspace{3mm} \\
\frac{\Gamma \vdash T : \mathrm{Type} \qquad \Gamma\left[x : T\right] \vdash T' : xs}{\Gamma \vdash \Pi x : T . T' : s} \text{,} \vspace{3mm} \\
\frac{\Gamma \vdash \Pi x : T . T' : s \qquad \Gamma\left[x : T\right] \vdash t : T'}{\Gamma \vdash \lambda x : T . t : \Pi x : T . T'} \text{,} \vspace{3mm} \\
\frac{\Gamma \vdash t : \Pi x : T . T' \qquad \Gamma \vdash t' : T}{\Gamma \vdash \left(t\ t'\right) : T'\left[x \leftarrow t'\right]} \text{,} \vspace{3mm} \\
