stan/Ecoop2024_TIforWildFJ
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Start variables keep in scope lemma

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-08-02 01:10:46 +02:00
parent 550bc384e5
commit 454cbab6db
1 changed files with 6 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
soundness.tex
View File

@ -156,6 +156,12 @@ We have to show T-Let and T-Call which leaves us with:
\end{description} \end{description}
\begin{lemma}
Free variables never leave their scope.
If $\tv{e} \lessdot \tv{x}, \overline{\tv{e} \lessdot \tv{x}},
\tv{r} \lessdot \tv{a}$ % TODO
\end{lemma}
% \begin{lemma} Unify does add free variables to types not containing free variables (or wildcard placeholders) % \begin{lemma} Unify does add free variables to types not containing free variables (or wildcard placeholders)
% \begin{description} % \begin{description}
% \item[If] $(\sigma, \Delta) = \unify{}( \Delta', C )$ % \item[If] $(\sigma, \Delta) = \unify{}( \Delta', C )$