Commit 3be82ddc authored by Mickael Laurent's avatar Mickael Laurent
Browse files

minor clarification

parent c23f3b22
......@@ -85,7 +85,8 @@ In what follows we will omit the indexes $e$ and $\Gamma,e,t$ when they are clea
\begin{definition}
Given an expression $e$ and a type $t$ we use $\Gamma^p_{\Gamma,e,t}$ to denote the environment that maps every subterm $e'$ of $e$ to the type $\bigwedge_{\{\varpi\alt \occ e\varpi\equiv e'\}}\Gp p {\Gamma,e,t}(\varpi)$ and is undefined otherwise.
Given an expression $e$ and a type $t$ we use $\Gamma^p_{\Gamma,e,t}$ to denote the environment that maps every subterm $e'$ of $e$ such that $\exists \varpi. \occ e\varpi\equiv e'$
to the type $\bigwedge_{\{\varpi\alt \occ e\varpi\equiv e'\}}\Gp p {\Gamma,e,t}(\varpi)$, and is undefined otherwise.
\end{definition}
The reason for the definition above is that the same subterm of $e$
may occur several times in $e$ and therefore we can collect for every
......
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