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

Merge branch 'master' of gitlab.math.univ-paris-diderot.fr:beppe/occurrence-typing

parents fd937d1d 6ac5773b
......@@ -218,9 +218,9 @@ above to an environment that already is the result of $\Refinef$, and so on. The
algorithm should compute the type environment as a fixpoint of the
function $X\mapsto\Refine{e,t}{X}$. Unfortunately, an iteration of $\Refinef$ may
not converge. As an example, consider the (dumb) expression $\tcase
{x x}{\Any}{e_1}{e_2}$. If $x:\Any\to\Any$, then every iteration of
{x x}{\Any}{e_1}{e_2}$. If $x:\Any\to\Any$, then when refining the ``then'' branch, every iteration of
$\Refinef$ yields for $x$ a type strictly more precise than the type deduced in the
previous iteration.
previous iteration (because of the $\varpi.0$ case).
The solution we adopt in practice is to bound the number of iterations to some number $n_o$. This is obtained by the following definition of $\Refinef$\svvspace{-1mm}
......
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