Commit 1224f6d5 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

new version

parent f727aced
......@@ -72,6 +72,8 @@ Let $e$ be an expression, $t$ a type, $\Gamma$ a type environment, $\varpi\in\{0
\typep+\epsilon{\Gamma,e,t} & = & t\\
\typep-\epsilon{\Gamma,e,t} & = & \neg t\\
\typep{p}{\varpi.0}{\Gamma,e,t} & = & \arrow{\tyof{\occ e{\varpi.1}}\Gamma}{\typep p \varpi{\Gamma,e,t}}\\
\color{red} \typep{p}{\varpi.0}{\Gamma,e,t} & = & \color{red}(\arrow{\tyof{\occ e{\varpi.1}}\Gamma}{\typep p \varpi{\Gamma,e,t}})\setminus\\
&&\color{red}(\arrow{\tyof{\occ e{\varpi.1}}\Gamma}{((\tyof{\occ e{\varpi.0}}\Gamma\circ\tyof{\occ e{\varpi.1}}\Gamma)\setminus\typep{p}{\varpi}{\Gamma,e,t})})\\
\typep{p}{\varpi.1}{\Gamma,e,t} & = & \worra{\tyof{\occ e{\varpi.0}}\Gamma}{\typep p \varpi{\Gamma,e,t}}\\ \\
\Gp p {\Gamma,e,t}(\varpi) &=& \typep p \varpi{\Gamma,e,t} \wedge \tyof {\occ e\varpi}\Gamma\\
\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