@@ -23648,15 +23648,15 @@ \section*{Appendix: Algorithmic Subtyping}
2364823648
2364923649 then \SubtypeNE{T_0}{T_1} if{}f each of the following criteria is satisfied,
2365023650 where the $Z_i$ are fresh type variables with bounds
23651- $B_{0i} [Z_0/X_0, \ldots, Z_k/X_k]$:
23651+ $[Z_0/X_0, \ldots, Z_k/X_k]B_{0i} $:
2365223652
2365323653 \begin{itemize}
2365423654 \item $p \geq n$.
2365523655 \item $m \geq q$.
23656- \item \SubtypeNE{S_i [Z_0/Y_0, \ldots, Z_k/Y_k]}{V_i [Z_0/X_0, \ldots, Z_k/X_k]}
23656+ \item \SubtypeNE{[Z_0/Y_0, \ldots, Z_k/Y_k]S_i}{ [Z_0/X_0, \ldots, Z_k/X_k]V_i }
2365723657 for $i \in 0 .. q$.
23658- \item \SubtypeNE{U_0 [Z_0/X_0, \ldots, Z_k/X_k]}{U_1 [Z_0/Y_0, \ldots, Z_k/Y_k]}.
23659- \item $B_{0i} [Z_0/X_0, \ldots, Z_k/X_k]$ and $B_{1i} [Z_0/Y_0, \ldots, Z_k/Y_k]$
23658+ \item \SubtypeNE{[Z_0/X_0, \ldots, Z_k/X_k]U_0}{ [Z_0/Y_0, \ldots, Z_k/Y_k]U_1 }.
23659+ \item $[Z_0/X_0, \ldots, Z_k/X_k]B_{0i} $ and $[Z_0/Y_0, \ldots, Z_k/Y_k]B_{1i} $
2366023660 have the same canonical syntax, for $i \in 0 .. k$.
2366123661 \end{itemize}
2366223662\item
@@ -23681,23 +23681,23 @@ \section*{Appendix: Algorithmic Subtyping}
2368123681 where $r_{1j}$ is empty or \REQUIRED{} for $j \in n+1 .. q$
2368223682 then \SubtypeNE{T_0}{T_1} if{}f the following criteria are all satisfied,
2368323683 where \List{Z}{1}{k} are fresh type variables with bounds
23684- $B_{0i} [Z_0/X_0, \ldots, Z_k/X_k]$:
23684+ $[Z_0/X_0, \ldots, Z_k/X_k]B_{0i} $:
2368523685
2368623686 \begin{itemize}
2368723687 \item
2368823688 $\{ y_{n+1}, \ldots, y_q \} \subseteq \{ x_{n+1}, \ldots , x_m \}$.
2368923689 \item
23690- \SubtypeNE{S_i [Z_0/Y_0, \ldots, Z_k/Y_k]}{V_i [Z_0/X_0, \ldots, Z_k/X_k]}
23690+ \SubtypeNE{[Z_0/Y_0, \ldots, Z_k/Y_k]S_i}{ [Z_0/X_0, \ldots, Z_k/X_k]V_i }
2369123691 for $i \in 0 .. n$.
23692- \item \SubtypeNE{S_i [Z_0/Y_0, \ldots, Z_k/Y_k]}{V_j [Z_0/X_0, \ldots, Z_k/X_k]}
23692+ \item \SubtypeNE{[Z_0/Y_0, \ldots, Z_k/Y_k]S_i}{ [Z_0/X_0, \ldots, Z_k/X_k]V_j }
2369323693 for $i \in n+1 .. q$, and $y_j = x_i$.
2369423694 \item
2369523695 for each $j$ such that $r_{0j}$ is \REQUIRED, there exists an
2369623696 $i \in n+1 .. q$ such that $x_j = y_i$, and $r_{1i}$ is \REQUIRED.
2369723697 \item
23698- \SubtypeNE{U_0 [Z_0/X_0, \ldots, Z_k/X_k]}{U_1 [Z_0/Y_0, \ldots, Z_k/Y_k]}.
23698+ \SubtypeNE{[Z_0/X_0, \ldots, Z_k/X_k]U_0}{ [Z_0/Y_0, \ldots, Z_k/Y_k]U_1 }.
2369923699 \item
23700- $B_{0i} [Z_0/X_0, \ldots, Z_k/X_k]$ and $B_{1i} [Z_0/Y_0, \ldots, Z_k/Y_k]$
23700+ $[Z_0/X_0, \ldots, Z_k/X_k]B_{0i} $ and $[Z_0/Y_0, \ldots, Z_k/Y_k]B_{1i} $
2370123701 have the same canonical syntax,
2370223702 for each $i \in 0 .. k$.
2370323703 \end{itemize}
0 commit comments