Commit 4ac30fbf authored by Mickael Laurent's avatar Mickael Laurent
Browse files

update algorithmic type system

parent 65e90d07
......@@ -309,8 +309,8 @@ We suppose w.l.o.g that all variables abstracted in $\lambda$-abstractions are d
{ \text{With priority over other rules} }
\\
\Infer[Occ]
{ \Gamma\setminus\{e\} \vdash e : t }
{ \Gamma \vdash e: \Gamma(e) \tsand t }
{ \Gamma\setminus\{e\} \vdash e : \ts }
{ \Gamma \vdash e: \Gamma(e) \tsand \ts }
{ e\in\dom\Gamma}
\qquad
\Infer[Const]
......@@ -384,7 +384,9 @@ We suppose w.l.o.g that all variables abstracted in $\lambda$-abstractions are d
\begin{align*}
&(\RefineStep p {e,t} (\Gamma))(e') =
\left\{\begin{array}{ll}
\tyof {e'} \Gamma \tsand \bigwedge_{\{\varpi \alt \occ e \varpi \equiv e'\}} \Gp p {\Gamma,e,t} (\varpi) & \text{if } \exists \varpi.\ \occ e \varpi \equiv e' \\
%\tyof {e'} \Gamma \tsand
\bigwedge_{\{\varpi \alt \occ e \varpi \equiv e'\}}
\Gp p {\Gamma,e,t} (\varpi) & \text{if } \exists \varpi.\ \occ e \varpi \equiv e' \\
\Gamma(e') & \text{otherwise, if } e' \in \dom \Gamma\\
\text{undefined} & \text{otherwise}
\end{array}\right.\\
......
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