Commit 41bc21f7 authored by Mickael Laurent's avatar Mickael Laurent
Browse files


parent b744911d
......@@ -429,7 +429,7 @@ TODO: Algorithmic rules
\Gamma,(x:s)\vdash e\triangleright_x\dt\\
\dt' = \dt\cup\{s\setminus\textstyle\bigcup_{u\in\dt}u\}\\
\forall u\in \dt'.\ \Gamma\bvdash{a}{u} \{t_u^i, \Gamma_u^i\}_{i\in I_u}\\
\forall u\in \dt'.\ \forall i\in I_u.\ \Gamma\ubvdash{u}{\letexp{x}{a}{e}}{t} \{(t_i^j,\Gamma_i^j)\}_{j\in J_i}}
\forall u\in \dt'.\ \forall i\in I_u.\ \Gamma_u^i\ubvdash{t_u^i}{\letexp{x}{a}{e}}{t} \{(t_i^j,\Gamma_i^j)\}_{j\in J_i}}
\Gamma\ubvdash{s}{\letexp{x}{a}{e}}{t} \bigcup_{u\in\dt'}\bigcup_{i\in I_u} \{(t_i^j,\Gamma_i^j)\}_{j\in J_i}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment