@@ -23499,15 +23499,15 @@ \section*{Appendix: Algorithmic Subtyping}
2349923499
2350023500 then \SubtypeNE{T_0}{T_1} if{}f each of the following criteria is satisfied,
2350123501 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} $:
2350323503
2350423504 \begin{itemize}
2350523505 \item $p \geq n$.
2350623506 \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 }
2350823508 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} $
2351123511 have the same canonical syntax, for $i \in 0 .. k$.
2351223512 \end{itemize}
2351323513\item
@@ -23532,23 +23532,23 @@ \section*{Appendix: Algorithmic Subtyping}
2353223532 where $r_{1j}$ is empty or \REQUIRED{} for $j \in n+1 .. q$
2353323533 then \SubtypeNE{T_0}{T_1} if{}f the following criteria are all satisfied,
2353423534 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} $:
2353623536
2353723537 \begin{itemize}
2353823538 \item
2353923539 $\{ y_{n+1}, \ldots, y_q \} \subseteq \{ x_{n+1}, \ldots , x_m \}$.
2354023540 \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 }
2354223542 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 }
2354423544 for $i \in n+1 .. q$, and $y_j = x_i$.
2354523545 \item
2354623546 for each $j$ such that $r_{0j}$ is \REQUIRED, there exists an
2354723547 $i \in n+1 .. q$ such that $x_j = y_i$, and $r_{1i}$ is \REQUIRED.
2354823548 \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 }.
2355023550 \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} $
2355223552 have the same canonical syntax,
2355323553 for each $i \in 0 .. k$.
2355423554 \end{itemize}
0 commit comments