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

minor fix

parent 2ff4839b
......@@ -114,12 +114,12 @@ functions as follows:
\Gamma,x:&\sigma\vdash e\triangleright\psi \qquad \qquad \Gamma,x:\sigma\vdash e:\tau\\
T = \{ (\sigma, \tau) \}
&\cup \{ (\sigma,\tau) ~|~ \sigma \in \psi(x) \land \Gamma, x: \sigma \vdash e: \tau \}\\
&\cup \{ (\sigma^*,\tau) ~|~ \sigma \in \psi(x) \land \Gamma, x: \sigma^* \vdash e: \tau \}
\Gamma\vdash\lambda x:\sigma.e:\textstyle\bigwedge_{(\sigma,\tau) \in T}\sigma\to \tau
......@@ -968,8 +968,8 @@
\begin{theorem}[Soundness of the algorithm]
&\forall \Gamma, e, t.\ \tyof e \Gamma \leq t \Rightarrow \Gamma \vdash e:t\\
&\forall \Gamma, e, t, \varpi.\ \pvdash \Gamma e t \varpi:\env {\Gamma,e,t} (\varpi)\\
&\forall \Gamma, e, t.\ \Gamma \evdash e t \Refine {e,t} \Gamma
&\forall \Gamma, e, t, \varpi.\ \tyof e \Gamma \neq \tsempty \Rightarrow \pvdash \Gamma e t \varpi:\env {\Gamma,e,t} (\varpi)\\
&\forall \Gamma, e, t.\ \tyof e \Gamma \neq \tsempty \Rightarrow \Gamma \evdash e t \Refine {e,t} \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