Make match rule remember constraint type

This commit is contained in:
Andreas Stadelmeier 2024-02-13 18:40:39 +01:00
parent fca93d7ec6
commit a0d98b9403

View File

@ -370,16 +370,16 @@ Their upper and lower bounds are fresh type variables.
\begin{array}[c]{@{}ll}
\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \, \set{
\tv{a} \lessdot \wctype{\Delta}{D}{\ol{T}}, \tv{a} \lessdot \wctype{\Delta'}{D'}{\ol{T'}} }\\
\tv{a} \lessdot_1 \wctype{\Delta}{D}{\ol{T}}, \tv{a} \lessdot_2 \wctype{\Delta'}{D'}{\ol{T'}} }\\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \vdash C \cup \, \left\{ \begin{array}[c]{l}
\tv{a} \lessdot \wctype{\overline{\wildcard{A}{\tv{u}}{\tv{l}}}}{C}{\overline{\rwildcard{A}}},
\ol{\tv{l}} \lessdot \ol{\tv{u}}, \\
\wctype{\overline{\wildcard{A}{\tv{u}}{\tv{l}}}}{C}{\overline{\rwildcard{A}}}
\lessdot \wctype{\Delta}{D}{\ol{T}}, \\
\lessdot_1 \wctype{\Delta}{D}{\ol{T}}, \\
\wctype{\overline{\wildcard{A}{\tv{u}}{\tv{l}}}}{C}{\overline{\rwildcard{A}}}
\lessdot \wctype{\Delta'}{D'}{\ol{T'}}
\lessdot_2 \wctype{\Delta'}{D'}{\ol{T'}}
\end{array}
\right\}
\end{array}