@@ -23664,15 +23664,15 @@ \section*{Appendix: Algorithmic Subtyping}
23664
23664
23665
23665
then \SubtypeNE{T_0}{T_1} if{}f each of the following criteria is satisfied,
23666
23666
where the $Z_i$ are fresh type variables with bounds
23667
- $B_{0i} [Z_0/X_0, \ldots, Z_k/X_k]$:
23667
+ $[Z_0/X_0, \ldots, Z_k/X_k]B_{0i} $:
23668
23668
23669
23669
\begin{itemize}
23670
23670
\item $p \geq n$.
23671
23671
\item $m \geq q$.
23672
- \item \SubtypeNE{S_i [Z_0/Y_0, \ldots, Z_k/Y_k]}{V_i [Z_0/X_0, \ldots, Z_k/X_k]}
23672
+ \item \SubtypeNE{[Z_0/Y_0, \ldots, Z_k/Y_k]S_i}{ [Z_0/X_0, \ldots, Z_k/X_k]V_i }
23673
23673
for $i \in 0 .. q$.
23674
- \item \SubtypeNE{U_0 [Z_0/X_0, \ldots, Z_k/X_k]}{U_1 [Z_0/Y_0, \ldots, Z_k/Y_k]}.
23675
- \item $B_{0i} [Z_0/X_0, \ldots, Z_k/X_k]$ and $B_{1i} [Z_0/Y_0, \ldots, Z_k/Y_k]$
23674
+ \item \SubtypeNE{[Z_0/X_0, \ldots, Z_k/X_k]U_0}{ [Z_0/Y_0, \ldots, Z_k/Y_k]U_1 }.
23675
+ \item $[Z_0/X_0, \ldots, Z_k/X_k]B_{0i} $ and $[Z_0/Y_0, \ldots, Z_k/Y_k]B_{1i} $
23676
23676
have the same canonical syntax, for $i \in 0 .. k$.
23677
23677
\end{itemize}
23678
23678
\item
@@ -23697,23 +23697,23 @@ \section*{Appendix: Algorithmic Subtyping}
23697
23697
where $r_{1j}$ is empty or \REQUIRED{} for $j \in n+1 .. q$
23698
23698
then \SubtypeNE{T_0}{T_1} if{}f the following criteria are all satisfied,
23699
23699
where \List{Z}{1}{k} are fresh type variables with bounds
23700
- $B_{0i} [Z_0/X_0, \ldots, Z_k/X_k]$:
23700
+ $[Z_0/X_0, \ldots, Z_k/X_k]B_{0i} $:
23701
23701
23702
23702
\begin{itemize}
23703
23703
\item
23704
23704
$\{ y_{n+1}, \ldots, y_q \} \subseteq \{ x_{n+1}, \ldots , x_m \}$.
23705
23705
\item
23706
- \SubtypeNE{S_i [Z_0/Y_0, \ldots, Z_k/Y_k]}{V_i [Z_0/X_0, \ldots, Z_k/X_k]}
23706
+ \SubtypeNE{[Z_0/Y_0, \ldots, Z_k/Y_k]S_i}{ [Z_0/X_0, \ldots, Z_k/X_k]V_i }
23707
23707
for $i \in 0 .. n$.
23708
- \item \SubtypeNE{S_i [Z_0/Y_0, \ldots, Z_k/Y_k]}{V_j [Z_0/X_0, \ldots, Z_k/X_k]}
23708
+ \item \SubtypeNE{[Z_0/Y_0, \ldots, Z_k/Y_k]S_i}{ [Z_0/X_0, \ldots, Z_k/X_k]V_j }
23709
23709
for $i \in n+1 .. q$, and $y_j = x_i$.
23710
23710
\item
23711
23711
for each $j$ such that $r_{0j}$ is \REQUIRED, there exists an
23712
23712
$i \in n+1 .. q$ such that $x_j = y_i$, and $r_{1i}$ is \REQUIRED.
23713
23713
\item
23714
- \SubtypeNE{U_0 [Z_0/X_0, \ldots, Z_k/X_k]}{U_1 [Z_0/Y_0, \ldots, Z_k/Y_k]}.
23714
+ \SubtypeNE{[Z_0/X_0, \ldots, Z_k/X_k]U_0}{ [Z_0/Y_0, \ldots, Z_k/Y_k]U_1 }.
23715
23715
\item
23716
- $B_{0i} [Z_0/X_0, \ldots, Z_k/X_k]$ and $B_{1i} [Z_0/Y_0, \ldots, Z_k/Y_k]$
23716
+ $[Z_0/X_0, \ldots, Z_k/X_k]B_{0i} $ and $[Z_0/Y_0, \ldots, Z_k/Y_k]B_{1i} $
23717
23717
have the same canonical syntax,
23718
23718
for each $i \in 0 .. k$.
23719
23719
\end{itemize}
0 commit comments