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

WF lemma

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-01-31 07:51:17 +01:00
parent 54fb6f9f0f
commit 8e3707b9a6
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
soundness.tex
View File

@ -163,8 +163,8 @@ Method calls generate multiple constraints that share the same wildcard placehol
\end{description}
\end{lemma}
Only the \rulename{General} rule generates fresh wildcards.
By lemma \ref{lemma:unifySoundness} we get $\Delta \vdash $
By S-Exists and S-Trans
By lemma \ref{lemma:unifySoundness} we get $\Delta \vdash \sigma(\type{T}) <: \sigma(\tv{a})$ with $\sigma(\tv{a}) = \wctype{\ol{\wildcard{X}{\sigma(U)}{\sigma(L)}}}{C}{\ol{X}}$
By S-Exists and S-Trans we can say $\Delta \vdash \sigma(\type{L}) <: \sigma(\type{U})$
% All types supplied to the Unify algorithm by TYPEs only contain ? extends or ? super wildcards. (X : [bot..T] or X : [T .. Object]).
% Both are well formed!