[−][src]Function voile::check::expr::check_row_polymorphic_type
fn check_row_polymorphic_type(
tcs: TCS,
info: Loc,
level: Level,
kind: VarRec,
variants: &[LabAbs],
ext: &Option<Box<Abs>>,
labels: &[String]
) -> ValTCM
Extracted from check.
$$
\newcommand{\ty}[0]{\tau}
\newcommand{\tyck}[4]{#1 \vdash_\texttt{c} #2 : #3 \Rightarrow #4}
\newcommand{\Gtyck}[3]{\tyck{\Gamma}{#1}{#2}{#3}}
\newcommand{\cheval}[3]{#1 \vdash_\texttt{e} #2 \Rightarrow #3}
\newcommand{\Gcheval}[2]{\cheval{\Gamma}{#1}{#2}}
\newcommand{\variant}[1]{\textbf{Sum}\ \{ #1 \}}
\newcommand{\record}[1]{\textbf{Rec}\ \{ #1 \}}
\newcommand{\variantR}[1]{\mathbb{Sum}\ #1}
\newcommand{\recordR}[1]{\mathbb{Rec}\ #1}
\newcommand{\variantextS}[2]{\variant{#1, \ldots = #2}}
\newcommand{\recordextS}[2]{\record{#1, \ldots = #2}}
\newcommand{\cA}[0]{\mathcal A}
\cfrac{
n \notin ns \quad \Gtyck{A}{\ty}{\cA}
}{
\cfrac{
\Gcheval{B}{\recordR{n,ns}}
}{
\Gcheval{\recordextS{n : A}{B}}{\recordR{ns}}
} \quad
\cfrac{
\Gcheval{B}{\variantR{n,ns}}
}{
\Gcheval{\variantextS{n : A}{B}}{\variantR{ns}}
}
}
\\
\cfrac{
}{
\Gtyck{\record{}}{\recordR{ns}}{\record{}} \quad
\Gtyck{\variant{}}{\variantR{ns}}{\variant{}}
}
$$