@@ -23664,15 +23664,15 @@ \section*{Appendix: Algorithmic Subtyping}
2366423664
2366523665 then \SubtypeNE{T_0}{T_1} if{}f each of the following criteria is satisfied,
2366623666 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} $:
2366823668
2366923669 \begin{itemize}
2367023670 \item $p \geq n$.
2367123671 \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 }
2367323673 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} $
2367623676 have the same canonical syntax, for $i \in 0 .. k$.
2367723677 \end{itemize}
2367823678\item
@@ -23697,23 +23697,23 @@ \section*{Appendix: Algorithmic Subtyping}
2369723697 where $r_{1j}$ is empty or \REQUIRED{} for $j \in n+1 .. q$
2369823698 then \SubtypeNE{T_0}{T_1} if{}f the following criteria are all satisfied,
2369923699 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} $:
2370123701
2370223702 \begin{itemize}
2370323703 \item
2370423704 $\{ y_{n+1}, \ldots, y_q \} \subseteq \{ x_{n+1}, \ldots , x_m \}$.
2370523705 \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 }
2370723707 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 }
2370923709 for $i \in n+1 .. q$, and $y_j = x_i$.
2371023710 \item
2371123711 for each $j$ such that $r_{0j}$ is \REQUIRED, there exists an
2371223712 $i \in n+1 .. q$ such that $x_j = y_i$, and $r_{1i}$ is \REQUIRED.
2371323713 \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 }.
2371523715 \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} $
2371723717 have the same canonical syntax,
2371823718 for each $i \in 0 .. k$.
2371923719 \end{itemize}
0 commit comments