Commit 6442e3d3 authored by Mickael Laurent's avatar Mickael Laurent
Browse files
parents 5ee8c94c 8a90ec4d
......@@ -206,7 +206,7 @@ well as the proof of its type safety.
\end{mathpar}
%
\begin{mathpar}
\textbf{Context rules:}\\
\textbf{Context reductions:}\\
\Infer[$\kappa$]
{e \xleadsto{e_r\mapsto e_r'} e'}
{C[e] \xleadsto{e_r\mapsto e_r'} C[e']}
......@@ -281,7 +281,7 @@ with
Finally, the only environments that we consider are well-formed environments (see definition below). We can easily
check that every derivation only contains well-formed environments, provided that the initial judgement also use a well-formed environment.
It is a consequence of the fact that rule \Rule{Case} require $e$ to be typeable and that it only refines subexpressions of $e$.
It is a consequence of the fact that rule \Rule{Case} requires $e$ to be typeable and that it only refines subexpressions of $e$.
\subsubsection{Environments}
......
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