Commit c274a79b authored by Mickael Laurent's avatar Mickael Laurent
Browse files

fix

parent 4ff9eff2
......@@ -416,10 +416,11 @@ TODO: Algorithmic rules
\\
\Infer[LetBase]
{
\Gamma,(x:s)\bvdash{e}{t} \{(t_i,\Gamma_i)\}_{i\in I}
\Gamma,(x:s)\bvdash{e}{t} \{(t_i,\Gamma_i)\}_{i\in I}\\
\forall i\in I.\ \Gamma_i\setminus\{x\}\bvdash{a}{\Gamma_i(x)} \{(t_i^j,\Gamma_i^j)\}_{j\in J_i}
}
{
\Gamma\ubvdash{s}{\letexp{x}{a}{e}}{t} \{(t_i,\Gamma_i)\}_{i\in I}
\Gamma\ubvdash{s}{\letexp{x}{a}{e}}{t} \{(t_i,\Gamma_i^j)\ \alt\ i\in I,\ 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