initSidebarItems({"fn":[["compile_cons","Evaluate a single constructor as a lambda."],["evaluate","Evaluation rules. $$ \\newcommand{\\xx}[0]{\\texttt{x}} \\newcommand{\\ty}[0]{\\tau} \\newcommand{\\eval}[1]{\\llbracket #1 \\rrbracket} % {\\texttt{eval}(#1)} \\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{\\variantR}[1]{\\mathbb{Sum}\\ #1} \\newcommand{\\recordR}[1]{\\mathbb{Rec}\\  #1} \\newcommand{\\cA}[0]{\\mathcal A} \\newcommand{\\cB}[0]{\\mathcal B} \\newcommand{\\labels}[1]{\\texttt{labels}(#1)} \\newcommand{\\fields}[1]{\\texttt{fields}(#1)} \\newcommand{\\tyLab}[0]{\\bar \\gamma} \\newcommand{\\labVal}[0]{\\bar \\delta} \\newcommand{\\ctyLab}[0]{\\gamma} \\newcommand{\\clabVal}[0]{\\delta} \\newcommand{\\caseTr}[0]{\\text{ct}} \\newcommand{\\caseS}[1]{\\langle #1 \\rangle} \\newcommand{\\case}[4]{\\textbf{case}\\ #1\\ #2: #3\\ \\textbf{or}\\ #4} \\newcommand{\\casevS}[2]{\\textbf{split}\\ #1\\ (#2)} \\newcommand{\\oneCase}[2]{#1\\ #2} \\newcommand{\\oneCaseL}[2]{\\oneCase{#1}{\\langle #2 \\rangle}} \\newcommand{\\caseextS}[2]{\\textbf{split}\\ (#1)\\ \\textbf{or}\\ #2} \\newcommand{\\nocases}[0]{\\textbf{whatever}} \\newcommand{\\recordext}[2]{\\record{#1 \\mid #2}} \\newcommand{\\recExt}[1]{\\mid #1} \\newcommand{\\variantextS}[2]{\\variant{#1, \\ldots = #2}} \\newcommand{\\recordextS}[2]{\\record{#1, \\ldots = #2}} \\newcommand{\\variantext}[2]{\\variant{#1 \\mid #2}} \\begin{alignedat}{2} & \\labels{\\emptyset} &&= \\emptyset \\\\ & \\labels{n : a, \\tyLab} &&= n : \\eval{a}, \\labels{\\tyLab} \\\\ & \\fields{\\emptyset} &&= \\emptyset \\\\ & \\fields{n = a, \\labVal} &&= n = \\eval{a}, \\fields{\\labVal} \\\\ & && \\\\ & \\eval{a, b} &&= \\eval{a}, \\eval{b} \\\\ & \\eval{a.1} &&= \\left\\{\\begin{matrix}   [k.1] & \\text{if} & \\eval{a} = [k] \\\\   \\alpha_0 & \\text{if} & \\eval{a} = \\alpha_0, \\alpha_1 \\end{matrix}\\right\\} \\\\ & \\eval{a.2} &&= \\left\\{\\begin{matrix}   [k.2] & \\text{if} & \\eval{a} = [k] \\\\   \\alpha_1 & \\text{if} & \\eval{a} = \\alpha_0, \\alpha_1 \\end{matrix}\\right\\} \\\\ & \\eval{\\lambda \\xx. a} &&= \\lambda \\langle \\xx . \\eval{a} \\rangle \\\\ & \\eval{\\xx} &&= [\\xx] \\\\ & \\eval{a\\ b} &&= \\left\\{\\begin{matrix}   [k\\ \\eval{b}] & \\text{if} & \\eval{a} = [k] \\\\   \\alpha [\\xx := \\eval{b}] & \\text{if} & \\eval{a} = \\lambda \\langle \\xx . \\alpha \\rangle   \\\\   \\left\\{\\begin{matrix}     \\alpha [\\xx := \\beta] & \\text{if} & \\eval{b} = n\\ \\beta \\\\     [\\casevS{k}{\\oneCaseL{n}{\\xx. \\alpha}, \\caseTr}] & \\text{if} & \\eval{b} = [k] \\\\   \\end{matrix}\\right\\} &   \\text{if} & \\eval{a} = \\lambda \\langle \\oneCaseL{n}{\\xx. \\alpha}, \\caseTr \\rangle \\end{matrix}\\right\\} \\\\ & \\eval{\\piTy{\\xx : a.b}} &&= \\Pi\\ \\eval{a}\\ \\langle \\xx . \\eval{b} \\rangle \\\\ & \\eval{\\sigTy{\\xx : a.b}} &&= \\Sigma\\ \\eval{a}\\ \\langle \\xx . \\eval{b} \\rangle \\\\ & \\eval{\\variantR{ns}} &&= \\variantR{ns} \\\\ & \\eval{\\recordR{ns}} &&= \\recordR{ns} \\\\ & \\eval{\\variant{\\tyLab}} &&= \\variant{\\labels{\\tyLab}} \\\\ & \\eval{\\record{\\tyLab}} &&= \\record{\\labels{\\tyLab}} \\\\ & \\eval{\\variantextS{\\tyLab_0}{a}} &&= \\left\\{\\begin{matrix}   [\\variantext{\\labels{\\tyLab_0}}{k}] & \\text{if} & \\eval{a} = [k] \\\\   \\variant{\\labels{\\tyLab_0} \\cup \\ctyLab_1} & \\text{if} & \\eval{a} = \\variant{\\ctyLab_1} \\\\   [\\variantext{\\labels{\\tyLab_0} \\cup \\ctyLab_1}{k}] & \\text{if} & \\eval{a} = [\\variantext{\\ctyLab_1}{k}] \\\\ \\end{matrix}\\right\\} \\\\ & \\eval{\\recordextS{\\tyLab_0}{a}} &&= \\left\\{\\begin{matrix}   [\\recordext{\\labels{\\tyLab_0}}{k}] & \\text{if} & \\eval{a} = [k] \\\\   \\record{\\labels{\\tyLab_0} \\cup \\ctyLab_1} & \\text{if} & \\eval{a} = \\record{\\ctyLab_1} \\\\   [\\recordext{\\labels{\\tyLab_0} \\cup \\ctyLab_1}{k}] & \\text{if} & \\eval{a} = [\\recordext{\\ctyLab_1}{k}] \\\\ \\end{matrix}\\right\\} \\\\ & \\eval{n\\ a} &&= n\\ \\eval{a} \\\\ & \\eval{\\{ \\labVal \\}} &&= \\{ \\fields{\\labVal} \\} \\\\ & \\eval{\\{ \\labVal_0\\recExt{a} \\}} &&= \\left\\{\\begin{matrix}   \\{ \\fields{\\labVal_0} \\cup \\clabVal_1 \\} & \\text{if} & \\eval{a} = \\{ \\clabVal_1 \\} \\\\   [\\{ \\fields{\\labVal_0} \\cup \\clabVal_1\\recExt{k} \\}] & \\text{if}      & \\eval{a} = [\\{ n = \\alpha, \\ctyLab_1\\recExt{k} \\}] \\\\   [\\{ \\fields{\\labVal_0}\\recExt{k} \\}] & \\text{if} & \\eval{a} = [k] \\\\ \\end{matrix}\\right\\} \\\\ & \\eval{a.n} &&= \\left\\{\\begin{matrix}   [k.n] & \\text{if} & \\eval{a} = [k] \\\\   \\alpha & \\text{if} & \\eval{a} = \\{ n = \\alpha, \\ctyLab \\} \\\\ \\end{matrix}\\right\\} \\\\ & \\eval{\\nocases} &&= \\lambda \\langle \\rangle \\\\ & \\eval{\\case{n}{\\xx}{a}{b}} &&= \\left\\{\\begin{matrix}   \\lambda \\langle \\oneCaseL{n}{\\xx. \\eval{a}}, \\caseTr \\rangle   & \\text{if} & \\eval{b} = \\lambda \\langle \\caseTr \\rangle \\\\   \\caseextS{\\oneCaseL{n}{\\xx. \\eval{a}}}{k} & \\text{if} & \\eval{b} = [k] \\\\ \\end{matrix}\\right\\} \\\\ & \\eval{\\ty} &&= \\ty \\end{alignedat} $$"],["evaluate_variants",""],["expand_global","Expand global references to concrete values, like meta references or global references due to recursion."]]});