@@ -23676,15 +23676,15 @@ \section*{Appendix: Algorithmic Subtyping}
2367623676
2367723677 then \SubtypeNE{T_0}{T_1} if{}f each of the following criteria is satisfied,
2367823678 where the $Z_i$ are fresh type variables with bounds
23679- $B_{0i} [Z_0/X_0, \ldots, Z_k/X_k]$:
23679+ $[Z_0/X_0, \ldots, Z_k/X_k]B_{0i} $:
2368023680
2368123681 \begin{itemize}
2368223682 \item $p \geq n$.
2368323683 \item $m \geq q$.
23684- \item \SubtypeNE{S_i [Z_0/Y_0, \ldots, Z_k/Y_k]}{V_i [Z_0/X_0, \ldots, Z_k/X_k]}
23684+ \item \SubtypeNE{[Z_0/Y_0, \ldots, Z_k/Y_k]S_i}{ [Z_0/X_0, \ldots, Z_k/X_k]V_i }
2368523685 for $i \in 0 .. q$.
23686- \item \SubtypeNE{U_0 [Z_0/X_0, \ldots, Z_k/X_k]}{U_1 [Z_0/Y_0, \ldots, Z_k/Y_k]}.
23687- \item $B_{0i} [Z_0/X_0, \ldots, Z_k/X_k]$ and $B_{1i} [Z_0/Y_0, \ldots, Z_k/Y_k]$
23686+ \item \SubtypeNE{[Z_0/X_0, \ldots, Z_k/X_k]U_0}{ [Z_0/Y_0, \ldots, Z_k/Y_k]U_1 }.
23687+ \item $[Z_0/X_0, \ldots, Z_k/X_k]B_{0i} $ and $[Z_0/Y_0, \ldots, Z_k/Y_k]B_{1i} $
2368823688 have the same canonical syntax, for $i \in 0 .. k$.
2368923689 \end{itemize}
2369023690\item
@@ -23709,23 +23709,23 @@ \section*{Appendix: Algorithmic Subtyping}
2370923709 where $r_{1j}$ is empty or \REQUIRED{} for $j \in n+1 .. q$
2371023710 then \SubtypeNE{T_0}{T_1} if{}f the following criteria are all satisfied,
2371123711 where \List{Z}{1}{k} are fresh type variables with bounds
23712- $B_{0i} [Z_0/X_0, \ldots, Z_k/X_k]$:
23712+ $[Z_0/X_0, \ldots, Z_k/X_k]B_{0i} $:
2371323713
2371423714 \begin{itemize}
2371523715 \item
2371623716 $\{ y_{n+1}, \ldots, y_q \} \subseteq \{ x_{n+1}, \ldots , x_m \}$.
2371723717 \item
23718- \SubtypeNE{S_i [Z_0/Y_0, \ldots, Z_k/Y_k]}{V_i [Z_0/X_0, \ldots, Z_k/X_k]}
23718+ \SubtypeNE{[Z_0/Y_0, \ldots, Z_k/Y_k]S_i}{ [Z_0/X_0, \ldots, Z_k/X_k]V_i }
2371923719 for $i \in 0 .. n$.
23720- \item \SubtypeNE{S_i [Z_0/Y_0, \ldots, Z_k/Y_k]}{V_j [Z_0/X_0, \ldots, Z_k/X_k]}
23720+ \item \SubtypeNE{[Z_0/Y_0, \ldots, Z_k/Y_k]S_i}{ [Z_0/X_0, \ldots, Z_k/X_k]V_j }
2372123721 for $i \in n+1 .. q$, and $y_j = x_i$.
2372223722 \item
2372323723 for each $j$ such that $r_{0j}$ is \REQUIRED, there exists an
2372423724 $i \in n+1 .. q$ such that $x_j = y_i$, and $r_{1i}$ is \REQUIRED.
2372523725 \item
23726- \SubtypeNE{U_0 [Z_0/X_0, \ldots, Z_k/X_k]}{U_1 [Z_0/Y_0, \ldots, Z_k/Y_k]}.
23726+ \SubtypeNE{[Z_0/X_0, \ldots, Z_k/X_k]U_0}{ [Z_0/Y_0, \ldots, Z_k/Y_k]U_1 }.
2372723727 \item
23728- $B_{0i} [Z_0/X_0, \ldots, Z_k/X_k]$ and $B_{1i} [Z_0/Y_0, \ldots, Z_k/Y_k]$
23728+ $[Z_0/X_0, \ldots, Z_k/X_k]B_{0i} $ and $[Z_0/Y_0, \ldots, Z_k/Y_k]B_{1i} $
2372923729 have the same canonical syntax,
2373023730 for each $i \in 0 .. k$.
2373123731 \end{itemize}
0 commit comments