Commit 94bfb2a7 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

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

parents 49beef11 06d91497
......@@ -217,7 +217,7 @@
\end{definition}
\begin{definition}[(Pre)order on environments]
Let $\Gamma$ and $\Gamma'$ two environments. We say that $\Gamma' \leq \Gamma$ iff:
Let $\Gamma$ and $\Gamma'$ two environments. We write $\Gamma' \leq \Gamma$ iff:
\begin{align*}
&\Gamma'=\bot \text{ or } (\Gamma\neq\bot \text{ and } \forall e \in \dom \Gamma.\ \Gamma' \vdash e : \Gamma(e))
\end{align*}
......@@ -984,7 +984,7 @@
If $\Gamma = \bot$, we trivially have $\Gamma \vdash e:t$ with the rule \Rule{Efq}.
Let's assume $\Gamma \neq \bot$.
If $e=x$ a variable, then the last rule used is \Rule{Var\Aa}.
If $e=x$ is a variable, then the last rule used is \Rule{Var\Aa}.
We can derive $\Gamma \vdash x:t$ by using the rule \Rule{Env} and \Rule{Subs}.
So let's assume that $e$ is not a variable.
......@@ -1002,7 +1002,7 @@
\item[$e=x$] Already treated.
\item[$e=\lambda^{\bigwedge_{i\in I} \arrow {t_i}{s_i}}x.e'$]
The last rule is \Rule{Abs\Aa}.
We have $\arrow {t_i}{s_i} \leq t$.
We have $\bigwedge_{i\in I} \arrow {t_i}{s_i} \leq t$.
Using the definition of type schemes, let $t'=\bigwedge_{i\in I} \arrow {t_i}{s_i} \land \bigwedge_{j\in J} \neg \arrow {t'_j}{s'_j}$ such that $\Empty \neq t' \leq t$.
The induction hypothesis gives, for all $i\in I$, $\Gamma,x:s_i\vdash e':t_i$.
......
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