This page requires javascript to work

[][src]Function voile::check::unify::unify_variants

fn unify_variants(
    tcs: TCS,
    kind: VarRec,
    subset: &Variants,
    superset: &Variants
) -> TCM

Unify two row-polymorphic types. $$ \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{\ty}[0]{\tau} \newcommand{\cA}[0]{\mathcal A} \newcommand{\cB}[0]{\mathcal B} \newcommand{\ctyLab}[0]{\gamma} \newcommand{\clabVal}[0]{\delta} \newcommand{\variant}[1]{\textbf{Sum}\ \{ #1 \}} \newcommand{\record}[1]{\textbf{Rec}\ \{ #1 \}} \cfrac{ \Gtyck{A_0}{\ty}{\cA_0} \quad \Gtyck{A_1}{\ty}{\cA_1} \quad \Gvdash \cA_0 \simeq \cA_1 \quad (n : \cA_0) \notin \ctyLab_0 \quad (n : \cA_1) \notin \ctyLab_1 }{ \cfrac{ \Gvdash \record{\ctyLab_0} \simeq \record{\ctyLab_1} }{ \Gvdash \record{n : \cA_0, \ctyLab_0} \simeq \record{n : \cA_1, \ctyLab_1} } \quad \cfrac{ \Gvdash \variant{\ctyLab_0} \simeq \variant{\ctyLab_1} }{ \Gvdash \variant{n : \cA_0, \ctyLab_0} \simeq \variant{n : \cA_1, \ctyLab_1} } } $$