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


parent de066d0a
......@@ -15,7 +15,7 @@ arrow type constructor.
We introduce the following abbreviations for types: $
t_1 \land t_2 \eqdef \neg (\neg t_1 \vee \neg t_2)$,
$t_ 1 \setminus t_2 \eqdef t_1 \wedge \neg t_2$, $\Any \eqdef \neg \Empty$, and likewise for type frames.
$t_ 1 \setminus t_2 \eqdef t_1 \wedge \neg t_2$, $\Any \eqdef \neg \Empty$.
We refer to $ b $ and $ \to $ as \emph{type constructors}
and to $ \lor $, $ \land $, $ \lnot $, and $ \setminus $
......@@ -172,7 +172,7 @@ Let $e$ be an expression, $t$ a type, $\Gamma$ a type environment, $\varpi\in\{0
\text{undefined} & \text{otherwise}
&\Gaux {\varnothing} \Gamma = \Gamma\\
&\Gaux {\cons {(e,t)} \tenv} \Gamma = \Gaux \tenv {\Refine p {e,t} \Gamma}\\&\\
&\Gaux {\cons {(e,t,p)} \tenv} \Gamma = \Gaux \tenv {\Refine p {e,t} \Gamma}\\&\\
&\Genv \tenv \Gamma=\fixpoint_\Gamma (\Gaa \tenv)\qquad \text{(if defined)}
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