[−][src]Function voile::check::expr::subtype
fn subtype(tcs: TCS, sub: &Val, sup: &Val) -> TCM
Check if subtype is a subtype of supertype.
$$
\newcommand{\Gvdash}[0]{\Gamma \vdash}
\newcommand{\tyck}[4]{#1 \vdash_\texttt{c} #2 : #3 \Rightarrow #4}
\newcommand{\Gtyck}[3]{\tyck{\Gamma}{#1}{#2}{#3}}
\newcommand{\subt}[0]{<:}
\newcommand{\xx}[0]{\texttt{x}}
\newcommand{\ty}[0]{\tau}
\newcommand{\piTy}[1]{\Pi \langle #1 \rangle}
\newcommand{\sigTy}[1]{\Sigma \langle #1 \rangle}
\newcommand{\variant}[1]{\textbf{Sum}\ \{ #1 \}}
\newcommand{\record}[1]{\textbf{Rec}\ \{ #1 \}}
\newcommand{\cA}[0]{\mathcal A}
\newcommand{\cB}[0]{\mathcal B}
\newcommand{\ctyLab}[0]{\gamma}
\newcommand{\clabVal}[0]{\delta}
\newcommand{\recordext}[2]{\record{#1 \mid #2}}
\newcommand{\recExt}[1]{\mid #1}
\newcommand{\variantext}[2]{\variant{#1 \mid #2}}
\newcommand{\variantR}[1]{\mathbb{Sum}\ #1}
\newcommand{\recordR}[1]{\mathbb{Rec}\ #1}
\cfrac{
\Gvdash \cA_0 \simeq \cA_1 \quad
\Gvdash \cB_0 \subt \cB_1
}{
\Gvdash \piTy{
\xx : \cA_0 . \cB_0
} \subt \piTy{\xx : \cA_1 . \cB_1} \quad
\Gvdash \sigTy{
\xx : \cA_0 . \cB_0
} \subt \sigTy{\xx : \cA_1 . \cB_1}
} \\ \space \\
\cfrac{
\Gvdash \cA_0 \subt \cA_1 \quad \Gvdash \cA_1 \subt \cA_2
}{
\Gvdash \cA_0 \subt \cA_2
} \quad
\cfrac{\Gvdash \cA \simeq \cB}{\Gvdash \cB \simeq \cA \quad \Gvdash \cA \subt \cB}
\\ \space \\
\cfrac{
n \notin ns
}{
\Gvdash \variantR{n,ns} \subt \variantR{ns} \quad
\Gvdash \recordR{ns} \subt \recordR{n,ns}
}
\\ \space \\
\cfrac{
\Gtyck{A}{\ty}{\cA} \quad
(n : \cA) \notin \ctyLab_0
}{
\cfrac{
\Gvdash \variant{\ctyLab_1} \subt \variant{\ctyLab_0}
}{
\Gvdash \variant{\ctyLab_1} \subt \variant{n : \cA, \ctyLab_0}
} \quad
\cfrac{
\Gvdash \record{\ctyLab_0} \subt \record{\ctyLab_1}
}{
\Gvdash \record{n : \cA, \ctyLab_0} \subt \record{\ctyLab_1}
}
}
\\
\cfrac{
}{
\Gvdash \recordR{ns} \subt \ty \quad
\Gvdash \variantR{ns} \subt \ty
}
$$