Pattern Typing

$$\infer{\Gamma \vdash \_ \leadsto \Gamma; \tau}{} \quad \infer{\Ga... ..., x : \tau; \tau}{} \quad \infer{\Gamma \vdash \ell \leadsto \Gamma; T(\ell)}{}$$

$$\infer{\Gamma \vdash X \leadsto \Gamma; \overline{[x_i \mapsto \t... ...a & \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau'' }$$

$$\infer{\Gamma \vdash M.X \leadsto \Gamma; \overline{[x_i \mapsto ... ...overline{x ::: \mathsf{Type}} \to \tau & \textrm{$\tau$ not a function type} }$$

$$\infer{\Gamma \vdash M.X \; p \leadsto \Gamma'; \overline{[x_i \m... ...u & \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau'' }$$

$$\infer{\Gamma \vdash \{\overline{x = p}\} \leadsto \Gamma_n; \{\o... ...ma_0 = \Gamma & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i }$$

$$\infer{\Gamma \vdash p : \tau \leadsto \Gamma'; \tau}{ \Gamma \vdash p \leadsto \Gamma'; \tau' & \Gamma \vdash \tau' \equiv \tau }$$