@@ -23648,15 +23648,15 @@ \section*{Appendix: Algorithmic Subtyping}
23648
23648
23649
23649
then \SubtypeNE{T_0}{T_1} if{}f each of the following criteria is satisfied,
23650
23650
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} $:
23652
23652
23653
23653
\begin{itemize}
23654
23654
\item $p \geq n$.
23655
23655
\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 }
23657
23657
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} $
23660
23660
have the same canonical syntax, for $i \in 0 .. k$.
23661
23661
\end{itemize}
23662
23662
\item
@@ -23681,23 +23681,23 @@ \section*{Appendix: Algorithmic Subtyping}
23681
23681
where $r_{1j}$ is empty or \REQUIRED{} for $j \in n+1 .. q$
23682
23682
then \SubtypeNE{T_0}{T_1} if{}f the following criteria are all satisfied,
23683
23683
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} $:
23685
23685
23686
23686
\begin{itemize}
23687
23687
\item
23688
23688
$\{ y_{n+1}, \ldots, y_q \} \subseteq \{ x_{n+1}, \ldots , x_m \}$.
23689
23689
\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 }
23691
23691
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 }
23693
23693
for $i \in n+1 .. q$, and $y_j = x_i$.
23694
23694
\item
23695
23695
for each $j$ such that $r_{0j}$ is \REQUIRED, there exists an
23696
23696
$i \in n+1 .. q$ such that $x_j = y_i$, and $r_{1i}$ is \REQUIRED.
23697
23697
\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 }.
23699
23699
\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} $
23701
23701
have the same canonical syntax,
23702
23702
for each $i \in 0 .. k$.
23703
23703
\end{itemize}
0 commit comments