113
правок
Изменения
→\lambda\Pi-исчисление
</tex>
где <tex>s ::= \mathrm{Type} \mid \mathrm{Kind}</tex>, а <tex>\mathrm{WF}</tex> {{---}} множество корректных грамматикконтекстов.
Терм <tex>t</tex> '''типизируется''' (англ. ''well-typed'') в контексте <tex>\Gamma</tex>, если существует такой терм <tex>T</tex>, что <tex>\Gamma \vdash t : T</tex>.}}
