@@ -23499,15 +23499,15 @@ \section*{Appendix: Algorithmic Subtyping}
23499
23499
23500
23500
then \SubtypeNE{T_0}{T_1} if{}f each of the following criteria is satisfied,
23501
23501
where the $Z_i$ are fresh type variables with bounds
23502
- $B_{0i} [Z_0/X_0, \ldots, Z_k/X_k]$:
23502
+ $[Z_0/X_0, \ldots, Z_k/X_k]B_{0i} $:
23503
23503
23504
23504
\begin{itemize}
23505
23505
\item $p \geq n$.
23506
23506
\item $m \geq q$.
23507
- \item \SubtypeNE{S_i [Z_0/Y_0, \ldots, Z_k/Y_k]}{V_i [Z_0/X_0, \ldots, Z_k/X_k]}
23507
+ \item \SubtypeNE{[Z_0/Y_0, \ldots, Z_k/Y_k]S_i}{ [Z_0/X_0, \ldots, Z_k/X_k]V_i }
23508
23508
for $i \in 0 .. q$.
23509
- \item \SubtypeNE{U_0 [Z_0/X_0, \ldots, Z_k/X_k]}{U_1 [Z_0/Y_0, \ldots, Z_k/Y_k]}.
23510
- \item $B_{0i} [Z_0/X_0, \ldots, Z_k/X_k]$ and $B_{1i} [Z_0/Y_0, \ldots, Z_k/Y_k]$
23509
+ \item \SubtypeNE{[Z_0/X_0, \ldots, Z_k/X_k]U_0}{ [Z_0/Y_0, \ldots, Z_k/Y_k]U_1 }.
23510
+ \item $[Z_0/X_0, \ldots, Z_k/X_k]B_{0i} $ and $[Z_0/Y_0, \ldots, Z_k/Y_k]B_{1i} $
23511
23511
have the same canonical syntax, for $i \in 0 .. k$.
23512
23512
\end{itemize}
23513
23513
\item
@@ -23532,23 +23532,23 @@ \section*{Appendix: Algorithmic Subtyping}
23532
23532
where $r_{1j}$ is empty or \REQUIRED{} for $j \in n+1 .. q$
23533
23533
then \SubtypeNE{T_0}{T_1} if{}f the following criteria are all satisfied,
23534
23534
where \List{Z}{1}{k} are fresh type variables with bounds
23535
- $B_{0i} [Z_0/X_0, \ldots, Z_k/X_k]$:
23535
+ $[Z_0/X_0, \ldots, Z_k/X_k]B_{0i} $:
23536
23536
23537
23537
\begin{itemize}
23538
23538
\item
23539
23539
$\{ y_{n+1}, \ldots, y_q \} \subseteq \{ x_{n+1}, \ldots , x_m \}$.
23540
23540
\item
23541
- \SubtypeNE{S_i [Z_0/Y_0, \ldots, Z_k/Y_k]}{V_i [Z_0/X_0, \ldots, Z_k/X_k]}
23541
+ \SubtypeNE{[Z_0/Y_0, \ldots, Z_k/Y_k]S_i}{ [Z_0/X_0, \ldots, Z_k/X_k]V_i }
23542
23542
for $i \in 0 .. n$.
23543
- \item \SubtypeNE{S_i [Z_0/Y_0, \ldots, Z_k/Y_k]}{V_j [Z_0/X_0, \ldots, Z_k/X_k]}
23543
+ \item \SubtypeNE{[Z_0/Y_0, \ldots, Z_k/Y_k]S_i}{ [Z_0/X_0, \ldots, Z_k/X_k]V_j }
23544
23544
for $i \in n+1 .. q$, and $y_j = x_i$.
23545
23545
\item
23546
23546
for each $j$ such that $r_{0j}$ is \REQUIRED, there exists an
23547
23547
$i \in n+1 .. q$ such that $x_j = y_i$, and $r_{1i}$ is \REQUIRED.
23548
23548
\item
23549
- \SubtypeNE{U_0 [Z_0/X_0, \ldots, Z_k/X_k]}{U_1 [Z_0/Y_0, \ldots, Z_k/Y_k]}.
23549
+ \SubtypeNE{[Z_0/X_0, \ldots, Z_k/X_k]U_0}{ [Z_0/Y_0, \ldots, Z_k/Y_k]U_1 }.
23550
23550
\item
23551
- $B_{0i} [Z_0/X_0, \ldots, Z_k/X_k]$ and $B_{1i} [Z_0/Y_0, \ldots, Z_k/Y_k]$
23551
+ $[Z_0/X_0, \ldots, Z_k/X_k]B_{0i} $ and $[Z_0/Y_0, \ldots, Z_k/Y_k]B_{1i} $
23552
23552
have the same canonical syntax,
23553
23553
for each $i \in 0 .. k$.
23554
23554
\end{itemize}
0 commit comments