Kinding

We write $[X \mapsto \kappa_1]\kappa_2$ for capture-avoiding substitution of $\kappa_1$ for $X$ in $\kappa_2$ .

$$\infer{\Gamma \vdash (c) :: \kappa :: \kappa}{ \Gamma \vdash c :... ...\Gamma } \quad \infer{\Gamma \vdash x :: \kappa}{ x :: \kappa = c \in \Gamma }$$

$$\infer{\Gamma \vdash M.x :: \kappa}{ \Gamma \vdash M : \mathsf{s... ...athsf{end} & \mathsf{proj}(M, \overline{s}, \mathsf{con} \; x) = (\kappa, c) }$$

$$\infer{\Gamma \vdash \tau_1 \to \tau_2 :: \mathsf{Type}}{ \Gamma... ...er{\Gamma \vdash \$c :: \mathsf{Type}}{ \Gamma \vdash c :: \{\mathsf{Type}\} }$$

$$\infer{\Gamma \vdash c_1 \; c_2 :: \kappa_2}{ \Gamma \vdash c_1 ... ...rrow c :: \kappa_1 \to \kappa_2}{ \Gamma, x :: \kappa_1 \vdash c :: \kappa_2 }$$

$$\infer{\Gamma \vdash c[\kappa'] :: [X \mapsto \kappa']\kappa}{ \... ...ma \vdash X \Longrightarrow c :: X \to \kappa}{ \Gamma, X \vdash c :: \kappa }$$

$$\infer{\Gamma \vdash () :: \mathsf{Unit}}{} \quad \infer{\Gamma \vdash \char93 X :: \mathsf{Name}}{}$$

$$\infer{\Gamma \vdash [\overline{c_i = c'_i}] :: \{\kappa\}}{ \fo... ...: \{\kappa\} & \Gamma \vdash c_2 :: \{\kappa\} & \Gamma \vdash c_1 \sim c_2 }$$

$$\infer{\Gamma \vdash \mathsf{map} :: (\kappa_1 \to \kappa_2) \to \{\kappa_1\} \to \{\kappa_2\}}{}$$

$$\infer{\Gamma \vdash (\overline c) :: (\kappa_1 \times \ldots \ti... ....i :: \kappa_i}{ \Gamma \vdash c :: (\kappa_1 \times \ldots \times \kappa_n) }$$

$$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow \tau :: \... ...vdash c_2 :: \{\kappa'\} & \Gamma, c_1 \sim c_2 \vdash \tau :: \mathsf{Type} }$$