113
правок
Изменения
→\lambda\Pi-исчисление: пояснил за well-formed.
<tex>
\displaystyle
\frac{}{\left[ \right] \textin \mathrm{ well-formedWF}} \text{,} \vspace{3mm} \\\frac{\Gamma \vdash T : s}{\Gamma\left[x : T\right] \textin \mathrm{ well-formedWF}} \text{,} \vspace{3mm} \\\frac{\Gamma \textin \mathrm{ well-formedWF}}{\Gamma \vdash \mathrm{Type} : \mathrm{Kind}} \text{,} \vspace{3mm} \\\frac{\Gamma \textin \mathrm{ well-formedWF} \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' : x}{\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} \\
</tex>
где <tex>s ::= \mathrm{Type} \mid \mathrm{Kind}</tex>, а <tex>\mathrm{WF}</tex> {{---}} множество корректных грамматик.
Терм <tex>t</tex> '''типизируется''' в контексте <tex>\Gamma</tex>, если существует такой терм <tex>T</tex>, что <tex>\Gamma \vdash t : T</tex>.}}
