Commit 34d69b94 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

some typos

parent 6992e639
......@@ -314,7 +314,7 @@ for the multiple occurrences of it.
satisfies progress and type preservation. The latter property is
challenging in our system because, as explained just above, our type
assumptions are not only about variables but also about
expressions. Two corner cases are particular difficult. The first is
expressions. Two corner cases are particularly difficult. The first is
shown by the following example
\begin{equation}\label{bistwo}
\ifty{e(42)}{\Int}{e}{...}
......
......@@ -181,7 +181,7 @@ Let $e$ be an expression, $t$ a type, $\Gamma$ a type environment, $\varpi\in\{0
\text{If } e \in \dom \Gamma \text{, } & \tyof x \Gamma &=& \Gamma(x)\\
& \tyof e \Gamma &=& \Gamma(e) \tsand \tyof e {\Gamma\setminus\{e\}}\\
\text{Otherwise,} & \tyof c \Gamma &=& \basic{c}\\
&\tyof {\lambda^{t}x.e} \Gamma &=& t\\
&\tyof {\lambda^{\bigwedge_{i\in I} \arrow {s_i} {t_i}}x.e} \Gamma &=& \tsfun {\arrow {s_i} {t_i}}_{i\in I}\\
&\tyof {{e_1} {e_2}} \Gamma &=& \apply {\tyof {e_1} \Gamma} {\tyof {e_2} \Gamma} & \text{(if defined)}\\
&\tyof {\pi_i e} \Gamma &=& \bpi_{\mathbf{i}}(\tyof e \Gamma) & \text{(if defined)}\\
&\tyof {(e_1,e_2)} \Gamma &=& \tyof {e_1} \Gamma \tstimes \tyof {e_2} \Gamma\\%\pair{\tyof {e_1} \Gamma}{\tyof {e_2} \Gamma}
......@@ -245,7 +245,7 @@ $s_2$ and thus their intersection $s_1{\wedge}s_2$.\\
\Infer[Abs]
{\tenv,\Gamma,x:s_i\vdash e:\ts_i'\\ \ts_i'\leq t_i}
{
\tenv,\Gamma\vdash\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:\textstyle\bigwedge_{i\in I}\arrow {s_i} {t_i}
\tenv,\Gamma\vdash\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:\textstyle\tsfun {\arrow {s_i} {t_i}}_{i\in I}
}
{\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e\not\in\dom\Gamma}
\\
......
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