Commit 1cfec5a7 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files


parent b7536bf7
......@@ -237,7 +237,7 @@ The solution we adopt in practice is to bound the number of iterations to some
Note in particular that $\Refine{e,t}\Gamma$ extends $\Gamma$ with hypotheses on the expressions occurring in $e$, since
$\dom{\Refine{e,t}\Gamma} = \dom{\RefineStep {e,t}(\Gamma)} = \dom{\Gamma} \cup \{e' \alt \exists \varpi.\ \occ e \varpi \equiv e'\}$.
$\dom{\Refine{e,t}\Gamma}$ $=$ $\dom{\RefineStep {e,t}(\Gamma)} = \dom{\Gamma} \cup \{e' \alt \exists \varpi.\ \occ e \varpi \equiv e'\}$.
In other terms, we try to find a fixpoint of $\RefineStep{e,t}$ but we
bound our search to $n_o$ iterations. Since $\RefineStep {e,t}$ is
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