Commit f3383c21 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files


parent 01795885
......@@ -849,7 +849,7 @@ of the type $\ts$ for $e$ cannot but end by a logical rule. Of course
this does not apply when the expression $e$ is a variable, since
an hypothesis in $\Gamma$ is the only way to deduce the type of a
variable, which is why the algorithm reintroduces the classic rule
for variables (\Rule{Var\Aa}).
for variables.
The algorithmic system above is sound with respect to the deductive one of Section~\ref{sec:static}
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