Compare commits

...

2 Commits

Author SHA1 Message Date
JanUlrich
0c89f28b18 Comments 2024-04-03 21:01:32 +02:00
JanUlrich
41a01d3abc Fix S-Exists 2024-04-03 21:01:21 +02:00
2 changed files with 13 additions and 1 deletions

View File

@ -289,7 +289,7 @@ $\begin{array}{l}
\Delta', \Delta \vdash [\ol{T}/\ol{\type{X}}]\ol{L} <: \ol{T} \quad \quad
\Delta', \Delta \vdash \ol{T} <: [\ol{T}/\ol{\type{X}}]\ol{U} \\
\text{fv}(\ol{T}) \subseteq \text{dom}(\Delta, \Delta') \quad
\text{dom}(\Delta') \cap \text{fv}(\wctype{\ol{\wildcard{X}{U}{L}}}{C}{\ol{S}}) = \emptyset
\text{dom}(\Delta') \cap \text{fv}(\wcNtype{\ol{\wildcard{X}{U}{L}}}{N}) = \emptyset
\\
\hline
\vspace*{-0.3cm}\\

View File

@ -323,6 +323,18 @@ The \rulename{Ground} rule uses this concept to generate \texttt{extends} Wildca
\end{description}
%TODO new rules:
% b <. List<x?>
% ----------------
% b =. bot | b <. List<x>
% b <. List<X>
% ----------------
% b =. bot | XU =. XL, a =. XU [a/X]C
% b =. C<X>
% --------------
% b =. X.C<X>
% \textbf{Example:}
% \begin{displaymath}