Commit cbf16e4d authored by Mickael Laurent's avatar Mickael Laurent
Browse files

remove useless type scheme lemma

parent 4ac30fbf
......@@ -103,12 +103,6 @@ Note that $\tsrep \ts \in \tsint \ts$.
\[\tsint {t \tsand \ts} = \{s \alt \exists t' \in \tsint \ts.\ t \land t' \leq s \}\]
\end{lemma}
\begin{lemma}[Intersection of type schemes]
Let $\ts_1$ and $\ts_2$ be two type schemes. We can compute a type scheme, written $\ts_1 \tsand \ts_2$, such that:
\[\tsint {\ts_1 \tsand \ts_2} = \{s\alt \exists t_1 \in \tsint {\ts_1}\
\exists t_2 \in \tsint {\ts_2}.\ {t_1} \land {t_2} \leq s\}\]
\end{lemma}
\begin{lemma}
Let $\ts$ be a type scheme and $t$ a type. We can decide the assertion $t \in \tsint \ts$,
which we also write $\ts \leq t$.
......@@ -123,7 +117,6 @@ Note that $\tsrep \ts \in \tsint \ts$.
\textbf{Expressions} & e & ::= & c\alt x \alt \lambda^{\bigwedge \arrow t t}x.e \alt \ite k t e e \alt e e\\
\textbf{Conditions} & k & ::= & c\alt x \alt \lambda^{\bigwedge \arrow t t}x.e \alt k k\\
\textbf{Values} & v & ::= & c \alt \lambda^{\bigwedge \arrow t t}x.e\\
\textbf{Occurrences} & o & ::= & c\alt x \alt \lambda^{\bigwedge \arrow t t}x.e \alt \ite k t e e \alt o o
\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