Commit 45c904a4 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

clarify refinestep

parent c6eda8ea
...@@ -754,7 +754,8 @@ From a formal point of view, this means to give up the completeness of the algor ...@@ -754,7 +754,8 @@ From a formal point of view, this means to give up the completeness of the algor
%\tyof {e'} \Gamma \tsand %\tyof {e'} \Gamma \tsand
\bigwedge_{\{\varpi \alt \occ e \varpi \equiv e'\}} \bigwedge_{\{\varpi \alt \occ e \varpi \equiv e'\}}
\env {\Gamma,e,t} (\varpi) & \text{if } \exists \varpi.\ \occ e \varpi \equiv e' \\ \env {\Gamma,e,t} (\varpi) & \text{if } \exists \varpi.\ \occ e \varpi \equiv e' \\
\Gamma(e') & \text{otherwise} \Gamma(e') & \text{otherwise, if } e'\in\dom\Gamma\\
\text{undefined} & \text{otherwise}
\end{array}\right. \end{array}\right.
\end{array} \end{array}
\] \]
......
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