macros.tex

% !TEX root = omar-thesis.tex
\newcommand{\dolla}{\texttt{\$}}  % used so I don't screw up syntax highlighting when using $ in an identifier inline

% \newcommand{\gheading}[1]{\multicolumn{3}{l}{\textbf{#1}}}

\newcommand{\elided}{{\color{gray}\cdots}}

\newcommand{\simplelang}{\textsf{\textbf{\small Calc}}}
\newcommand{\footnotesimplelang}{\textsf{\textbf{\footnotesize Algor}}}
\newcommand{\tnum}{\texttt{num}}
\newcommand{\numintro}[1]{\texttt{#1}}
\newcommand{\anumintro}[1]{\texttt{num}[#1]}
\newcommand{\aplus}[2]{\abop{plus}{#1; #2}}
\newcommand{\aminus}[2]{\abop{minus}{#1; #2}}
\newcommand{\amult}[2]{\abop{mult}{#1; #2}}
\newcommand{\adiv}[2]{\abop{div}{#1; #2}}
\newcommand{\apow}[2]{\abop{pow}{#1; #2}}

\newcommand{\letplain}[3]{\texttt{let}~#1=#2~\texttt{in}~#3}
\newcommand{\aletplain}[3]{\abop{let}{#1; #2.#3}}

% Calculi Names
\ificfp
\newcommand{\miniVerse}{{\lambda}_\textbf{TLM}}
\newcommand{\miniVerseUE}{\miniVerse^\textbf{SE}}
\newcommand{\miniVersePat}{\miniVerse^\textbf{S}}
\newcommand{\miniVerseParam}{\miniVerse^\textbf{P}}
\newcommand{\miniVerseTSL}{\mathsf{miniVerse}_\textbf{TSL}}
\newcommand{\miniVerseUB}{\miniVerse^\textbf{SB}}
\newcommand{\miniVersePH}{\miniVerse^\textbf{PH}}
\else
\newcommand{\miniVerse}{\mathsf{miniVerse}}
\newcommand{\miniVerseUE}{\mathsf{miniVerse}_\textbf{SE}}
\newcommand{\miniVersePat}{\mathsf{miniVerse}_\textbf{S}}
\newcommand{\miniVerseParam}{\mathsf{miniVerse}_\textbf{P}}
\newcommand{\miniVerseTSL}{\mathsf{miniVerse}_\textbf{TSL}}
\newcommand{\miniVerseUB}{\mathsf{miniVerse}_\textbf{S}^\textbf{B}}
\newcommand{\miniVersePH}{\mathsf{miniVerse}_\textbf{PH}}
\fi

% General abstract syntax
\newcommand{\aboppz}[2]{\texttt{#1}\texttt{[}#2\texttt{]}}
\newcommand{\abopbz}[2]{\texttt{#1}[#2]}
\newcommand{\abop}[2]{\texttt{#1}\texttt{(}#2\texttt{)}}
\newcommand{\abopi}[3]{\texttt{#1}[#2]\texttt{(}#3\texttt{)}}
\newcommand{\abopii}[4]{\texttt{#1}[#2][#3]\texttt{(}#4\texttt{)}}
\newcommand{\abopic}[4]{\texttt{#1}[#2]\texttt{\{}#3\texttt{\}(}#4\texttt{)}}
\newcommand{\abopp}[3]{\texttt{#1}\texttt{[}#2\texttt{](}#3\texttt{)}}
\newcommand{\abopc}[3]{\texttt{#1}\texttt{\{}#2\texttt{\}(}#3\texttt{)}}
\newcommand{\abopbc}[4]{\texttt{#1}\texttt{[}#2\texttt{]\{}#3\texttt{\}(}#4\texttt{)}}
\newcommand{\abopibc}[5]{\texttt{#1}[#2]\texttt{[}#3\texttt{]\{}#4\texttt{\}(}#5\texttt{)}}
\newcommand{\abopcc}[4]{\texttt{#1}\texttt{\{}#2\texttt{\}\{}#3\texttt{\}(}#4\texttt{)}}
\newcommand{\abopicz}[3]{\texttt{#1}[#2]\texttt{\{}#3\texttt{\}}}

% Types / candidate expansion types
\newcommand{\parr}[2]{#1 \rightharpoonup #2}
\newcommand{\aparr}[2]{\abop{parr}{#1; #2}}
\newcommand{\auparr}[2]{\abop{uparr}{#1; #2}}
\newcommand{\aceparr}[2]{\abop{prparr}{#1; #2}}

\newcommand{\forallt}[2]{\forall #1.#2}
\newcommand{\aall}[2]{\abop{all}{#1.#2}}
\newcommand{\auall}[2]{\abop{uall}{#1.#2}}
\newcommand{\aceall}[2]{\abop{prall}{#1.#2}}

\newcommand{\forallu}[3]{\forall(#1 :: #2).#3}
\newcommand{\aallu}[3]{\abopc{all}{#1}{#2.#3}}
\newcommand{\auallu}[3]{\abopc{uall}{#1}{#2.#3}}
\newcommand{\aceallu}[3]{\abopc{prall}{#1}{#2.#3}}

\newcommand{\rect}[2]{\mu #1.#2}
\newcommand{\arec}[2]{\abop{rec}{#1.#2}}
\newcommand{\aurec}[2]{\abop{urec}{#1.#2}}
\newcommand{\acerec}[2]{\abop{prrec}{#1.#2}}

\newcommand{\prodt}[1]{\langle #1 \rangle}
\newcommand{\aprod}[2]{\abopi{prod}{#1}{#2}}
\newcommand{\auprod}[2]{\abopi{uprod}{#1}{#2}}
\newcommand{\aceprod}[2]{\abopi{prprod}{#1}{#2}}

\newcommand{\sumt}[1]{[#1]}
\newcommand{\asum}[2]{\abopi{sum}{#1}{#2}}
\newcommand{\ausum}[2]{\abopi{usum}{#1}{#2}}
\newcommand{\acesum}[2]{\abopi{prsum}{#1}{#2}}

% Labels and maps
\newcommand{\labelset}{L}
\newcommand{\smapschema}[3]{\{#1_{#2}\}_{#2 \in #3}}
\newcommand{\mapschema}[3]{\{#2 \hookrightarrow #1_{#2}\}_{#2 \in #3}}
\newcommand{\mapschemab}[4]{\{#3 \hookrightarrow #1_{#3}.#2_{#3}\}_{#3 \in #4}}
\newcommand{\mapschemax}[4]{\{#3 \hookrightarrow #1(#2_{#3})\}_{#3 \in #4}}
\newcommand{\mapschemabx}[5]{\{#4 \hookrightarrow \sigilof{#2_{#4}}.#1(#3_{#4})\}_{#4 \in #5}}
\newcommand{\mapschemacx}[5]{\{#4 \hookrightarrow {#2_{#4}}.#1(#3_{#4})\}_{#4 \in #5}}
\newcommand{\finmap}[1]{#1}
\newcommand{\mapitem}[2]{#1 \hookrightarrow #2}
\newcommand{\lbltxt}[1]{\mathtt{#1}}

% sequences
\newcommand{\seqschema}[4]{\{#1_{#2}\}_{#3 \leq #2 \leq #4}}
\newcommand{\seqschemaijb}[8]{\{\{#1_{#3, #6}\}_{#7 \leq #6 < #8}.#2_{#3}\}_{#4 \leq #3 \leq #5}}
\newcommand{\seqschemaj}[4]{\{#1_{#2}\}_{#3 \leq #2 < #4}}
\newcommand{\seqschemaX}[1]{\seqschema{#1}{i}{1}{n}}
\newcommand{\seqschemaXx}[2]{\{#1(#2_i)\}_{1 \leq i \leq n}}
\newcommand{\seqschemajX}[1]{\seqschema{#1}{j}{1}{n}}

\newcommand{\sseq}[2]{\{#1\}_{0 \leq i < #2}}
\newcommand{\sseqS}[3]{\{#1\}_{#2 \leq i < #3}}

% Expanded/Unexpanded/Candidate expressions
\newcommand{\asc}[2]{#1 : #2}
\newcommand{\auasc}[2]{\abopc{uasc}{#1}{#2}}
\newcommand{\aceasc}[2]{\abopc{prasc}{#1}{#2}}

\newcommand{\letsyn}[3]{\texttt{let\,val}~#1=#2~\texttt{in}~#3}
\newcommand{\aletsyn}[3]{\abop{letval}{#2; #1.#3}}
\newcommand{\auletsyn}[3]{\abop{uletval}{#2; #1.#3}}
\newcommand{\aceletsyn}[3]{\abop{prletval}{#2; #1.#3}}

\newcommand{\analam}[2]{\lambda #1.#2}
\newcommand{\auanalam}[2]{\abop{uanalam}{#1.#2}}
\newcommand{\aceanalam}[2]{\abop{pranalam}{#1.#2}}

\newcommand{\lam}[3]{\lambda #1{:}#2.#3}
\newcommand{\aelam}[3]{\abopc{lam}{#1}{#2.#3}}
\newcommand{\aulam}[3]{\abopc{ulam}{#1}{#2.#3}}
\newcommand{\acelam}[3]{\abopc{prlam}{#1}{#2.#3}}

\newcommand{\ap}[2]{#1(#2)}
\newcommand{\aeap}[2]{\abop{ap}{#1; #2}}
\newcommand{\auap}[2]{\abop{uap}{#1; #2}}
\newcommand{\aceap}[2]{\abop{prap}{#1; #2}}

\newcommand{\Lam}[2]{\Lambda #1.#2}
\newcommand{\aetlam}[2]{\abop{tlam}{#1.#2}}
\newcommand{\autlam}[2]{\abop{utlam}{#1.#2}}
\newcommand{\acetlam}[2]{\abop{prtlam}{#1.#2}}

\newcommand{\App}[2]{#1\texttt{[}#2\texttt{]}}
\newcommand{\aetap}[2]{\abopc{tap}{#2}{#1}}
\newcommand{\autap}[2]{\abopc{utap}{#2}{#1}}
\newcommand{\acetap}[2]{\abopc{prtap}{#2}{#1}}

\newcommand{\clam}[3]{\Lambda #1{::}#2.#3}
\newcommand{\aeclam}[3]{\abopc{clam}{#1}{#2.#3}}
\newcommand{\auclam}[3]{\abopc{uclam}{#1}{#2.#3}}
\newcommand{\aceclam}[3]{\abopc{prclam}{#1}{#2.#3}}

\newcommand{\cAp}[2]{#1\texttt{[}#2\texttt{]}}
\newcommand{\aecap}[2]{\abopc{cap}{#2}{#1}}
\newcommand{\aucap}[2]{\abopc{ucap}{#2}{#1}}
\newcommand{\acecap}[2]{\abopc{prcap}{#2}{#1}}

\newcommand{\foldt}[2]{\texttt{fold}_{#1}(#2)}
\newcommand{\fold}[1]{\texttt{fold}(#1)}
\newcommand{\aefold}[1]{\abop{fold}{#1}}
\newcommand{\aufold}[3]{\abopc{ufold}{#1.#2}{#3}}
\newcommand{\acefold}[1]{\abop{prfold}{#1}}

\newcommand{\auanafold}[1]{\abop{ufold}{#1}}
\newcommand{\aceanafold}[1]{\abop{prfold}{#1}}

\newcommand{\unfold}[1]{\texttt{unfold}(#1)}
\newcommand{\aeunfold}[1]{\abop{unfold}{#1}}
\newcommand{\auunfold}[1]{\abop{uunfold}{#1}}
\newcommand{\aceunfold}[1]{\abop{prunfold}{#1}}

\newcommand{\tpl}[1]{\langle #1\rangle}
\newcommand{\aetpl}[2]{\abopi{tpl}{#1}{#2}}
\newcommand{\autpl}[2]{\abopc{utpl}{#1}{#2}}
\newcommand{\acetpl}[2]{\abopc{prtpl}{#1}{#2}}

\newcommand{\prj}[2]{#1 \cdot #2}
\newcommand{\aepr}[2]{\abopi{prj}{#1}{#2}}
\newcommand{\aupr}[2]{\abopi{uprj}{#1}{#2}}
\newcommand{\acepr}[2]{\abopi{prprj}{#1}{#2}}

\newcommand{\injt}[3]{\texttt{inj}_{#1}~#2 \cdot #3}
\newcommand{\inj}[2]{\texttt{inj}[#1](#2)}
\newcommand{\aein}[2]{\abopi{inj}{#1}{#2}}
\newcommand{\auin}[4]{\abopic{uinj}{#1; #2}{#3}{#4}}
\newcommand{\acein}[2]{\abopi{prinj}{#1}{#2}}

\newcommand{\auanain}[2]{\abopp{uin}{#1}{#2}}
\newcommand{\aceanain}[2]{\abopp{prinj}{#1}{#2}}

\newcommand{\caseof}[2]{\texttt{case}~#1~#2}
\newcommand{\aecase}[3]{\abopi{case}{#1}{#2; #3}}
\newcommand{\aucase}[4]{\abopic{ucase}{#1}{#2}{#3; #4}}
\newcommand{\acecase}[3]{\abopi{prcase}{#1}{#2; #3}}

% Expanded expressions
\newcommand{\etxt}[1]{e_\text{#1}}

\newcommand{\Uofv}{\mathcal{U}}
\newcommand{\Uof}[1]{\Uofv(#1)}
\newcommand{\sigilof}[1]{\widehat{#1}}
\newcommand{\VTypofv}{\mathcal{V}_\mathsf{Typ}}
\newcommand{\VTypof}[1]{\VTypofv(#1)}
\newcommand{\VExpofv}{\mathcal{V}_\mathsf{Exp}}
\newcommand{\VExpof}[1]{\VExpofv(#1)}
\newcommand{\Cofv}{\mathcal{P}}
\newcommand{\Cof}[1]{\Cofv(#1)}

% Statics of miniVerseU and miniVerseParam expanded expressions
\newcommand{\istypeU}[2]{#1 \vdash #2~\mathsf{type}}
\newcommand{\isctxU}[2]{#1 \vdash #2~\mathsf{ctx}}
\newcommand{\hastypeU}[4]{#1~#2 \vdash #3 : #4}
\newcommand{\hastypeUC}[2]{\vdash #1 : #2}
\newcommand{\hastypeUCO}[3]{#1 \vdash #2 : #3}

%\newcommand{\isctxP}[2]{#1 \vdash #2~\mathsf{ctx}}
\newcommand{\hastypeP}[3]{#1 \vdash #2 : #3}
\newcommand{\hastypePX}[2]{\hastypeP{\uOmega}{#1}{#2}}
\newcommand{\hastypePC}[2]{\vdash #1 : #2}

\newcommand{\Dhyp}[1]{#1~\mathsf{type}}
\newcommand{\Dcons}[2]{{#1}\cup{#2}}
\newcommand{\Ghyp}[2]{#1 : #2}
\newcommand{\Gcons}[2]{{#1}\cup{#2}}
\newcommand{\Gconsi}[2]{\cup_{#1} #2}
\newcommand{\GIconsi}[2]{\uplus_{#1} #2}
\newcommand{\Khyp}[1]{#1~\mathsf{kind}}

% Dynamics of miniVerseU
\newcommand{\isvalU}[1]{#1~\mathsf{val}}
\newcommand{\stepsU}[2]{#1 \mapsto #2}
\newcommand{\multistepU}[2]{#1 \mapsto^{*} #2}
\newcommand{\evalU}[2]{#1 \Downarrow #2}

% Unexpanded types
\newcommand{\utau}{{\hat\tau}}
\newcommand{\ut}{{\hat{t}}}
\newcommand{\uc}{{\hat c}}
\newcommand{\uu}{{\hat u}}

% Unexpanded kinds
\newcommand{\ukappa}{{\hat\kappa}}

% Unexpanded modules
\newcommand{\uM}{{\hat M}}
\newcommand{\usigma}{{\hat\sigma}}

% Unexpanded expressions
\newcommand{\ue}{{\hat e}}
\newcommand{\ux}{{\hat x}}
\newcommand{\uesyntax}[4]{\texttt{syntax}~#1~\texttt{at}~#2~\texttt{by}~\texttt{static}~#3~\texttt{in}~#4}
\newcommand{\uesyntaxq}[4]{\texttt{syntax}~#1~\texttt{at}~#2~\texttt{for}~\texttt{expressions}~\texttt{by}~\texttt{static}~#3~\texttt{in}~#4}

\newcommand{\audefuetsm}[4]{\abopcc{usyntaxse}{#2}{#1}{#3.#4}}
\newcommand{\utsmap}[2]{#1~\texttt{\lq}#2\texttt{\lq}}
\newcommand{\autsmap}[2]{\texttt{uapsetlm}[#1]\texttt{[}#2\texttt{]}}
\newcommand{\uet}[1]{\ue_\text{#1}}
\newcommand{\ueparse}{\uet{parse}}

% TLM expressions
\newcommand{\tsmv}{\hat{a}}
\newcommand{\utsmdef}[2]{\texttt{syntax}~@~#1~\texttt{\{}#2\texttt{\}}}
\newcommand{\istsmU}[2]{#1 \vdash #2~\mathsf{tlm}}

\newcommand{\uGamma}{\hat{\Gamma}}
\newcommand{\uDelta}{\hat{\Delta}}
\newcommand{\uD}{\mathcal{D}}
\newcommand{\uG}{\mathcal{G}}
\newcommand{\uDD}[2]{\langle #1; #2 \rangle}
\newcommand{\uGG}[2]{\langle #1; #2 \rangle}
\newcommand{\uGammaOK}[1]{\Delta \vdash #1~\mathsf{uctx}}
\newcommand{\uDeltaOK}[1]{#1 \vdash \mathsf{ok}}
\newcommand{\vExpands}[2]{#1 \leadsto #2}
\newcommand{\ctxUpdate}[3]{#1 \uplus \vExpands{#2}{#3}}
\newcommand{\uDhyp}[2]{#1 \leadsto #2~\mathsf{type}}
\newcommand{\uGhyp}[3]{#1 \leadsto #2 : #3}
\newcommand{\uGcons}[2]{#1 \uplus #2}

\newcommand{\uPsi}{\hat{\Psi}}
\newcommand{\uA}{\mathcal{A}}
\newcommand{\uAS}[2]{\langle #1; #2 \rangle}
\newcommand{\uShyp}[4]{#1 \leadsto #2 \hookrightarrow \xuetsmdef{#3}{#4}}
\newcommand{\pShyp}[4]{#1 \leadsto #2 \hookrightarrow \petsmdefn{#3}{#4}}
\newcommand{\uPhyp}[4]{#1 \leadsto #2 \hookrightarrow \xuptsmdef{#3}{#4}}
\newcommand{\pPhyp}[4]{#1 \leadsto #2 \hookrightarrow \pptsmdefn{#3}{#4}}

\newcommand{\tBody}{\mathtt{Body}}
\newcommand{\tParseResultExp}{\mathtt{ParseResultSE}} 
\newcommand{\tParseResultF}{\mathtt{ParseResult}}
\newcommand{\tParseResult}[1]{\mathtt{ParseResult}(#1)}
\newcommand{\tCEExp}{\mathtt{PrExpr}} % Typed expansion
\newcommand{\expandsU}[6]{#1~#2 \vdash_{#3} #4 \leadsto #5 : #6} % there's a multiline one in the document done manually
\newcommand{\expandsUX}[3]{\expandsU{\uDelta}{\uGamma}{\uPsi}{#1}{#2}{#3}}
\newcommand{\expandsUC}[3]{\vdash #1 \leadsto #2 : #3}
\newcommand{\expandsP}[6]{#1 \vdash_{#2; #3} #4 \leadsto #5 : #6}
\newcommand{\expandsPX}[3]{\expandsP{\uOmega}{\uPsi}{\uPhi}{#1}{#2}{#3}}
\newcommand{\expandsTU}[3]{#1 \vdash #2 \leadsto #3~\mathsf{type}}
\newcommand{\domof}[1]{\text{dom}(#1)}
\newcommand{\xuetsmdef}[2]{\abop{setlm}{#1;\,#2}}
\newcommand{\xuetsmbnd}[3]{#1 \hookrightarrow \xuetsmdef{#2}{#3}}
\newcommand{\uetsmenv}[2]{#1 \vdash #2~\mathsf{seTLMs}}
\newcommand{\petsmenv}[2]{#1 \vdash #2~\mathsf{peTLMs}}
\newcommand{\pptsmenv}[2]{#1 \vdash #2~\mathsf{ppTLMs}}
\newcommand{\uetsmctx}[2]{#1 \vdash #2~\mathsf{seTLMctx}}
\newcommand{\petsmctx}[2]{#1 \vdash #2~\mathsf{peTLMctx}}
\newcommand{\pptsmctx}[2]{#1 \vdash #2~\mathsf{ppTLMctx}}
\newcommand{\encodeBody}[2]{#1 \downarrow_\mathsf{Body} #2}
\newcommand{\decodeBody}[2]{#1 \uparrow_\mathsf{Body} #2}
\newcommand{\ebody}{\etxt{body}}
\newcommand{\eparse}{\etxt{parse}}
\newcommand{\ecand}{\etxt{proto}}
\newcommand{\decodeCondE}[2]{#1 \uparrow_\mathsf{PrExpr} #2}
\newcommand{\encodeCondE}[2]{#1 \downarrow_\mathsf{PrExpr} #2}

% Candidate Expansions
\newcommand{\ce}{\grave{e}}
\newcommand{\ctau}{\grave{\tau}}

\newcommand{\splicedt}[2]{\texttt{splicedt}[#1; #2]}
\newcommand{\asplicedt}[2]{\texttt{splicedt}[#1; #2]}
\newcommand{\acesplicedt}[2]{\texttt{splicedt}[#1; #2]}
\newcommand{\splicede}[3]{\texttt{splicede}[#1; #2; #3]}
\newcommand{\splicedet}[3]{\texttt{splicede}[#1; #2; #3]}
\newcommand{\asplicede}[2]{\texttt{splicede}[#1; #2]}
\newcommand{\acesplicede}[3]{\texttt{splicede}[#1; #2; #3]}
\newcommand{\acesplicedet}[3]{\texttt{anasplicede}[#1; #2]\texttt{\{}#3\texttt{\}}}
\newcommand{\splicedp}[3]{\texttt{splicedp}[#1; #2; #3]}
\newcommand{\acesplicedp}[3]{\texttt{splicedp}[#1; #2; #3]}
\newcommand{\splicedc}[3]{\texttt{splicedc}[#1; #2; #3]}
\newcommand{\acesplicedc}[3]{\texttt{splicedc}[#1; #2; #3]}
\newcommand{\splicedk}[2]{\texttt{splicedk}[#1; #2]}
\newcommand{\acesplicedk}[2]{\texttt{splicedk}[#1; #2]}

\newcommand{\mtau}{\dot{\tau}}
\newcommand{\mtspliced}[1]{\texttt{spliced}(#1)}

% Candidate expansion validation
\newcommand{\cvalidT}[4]{#1\vdash^{#2} #3 \leadsto #4~\mathsf{type}}
\newcommand{\cvalidE}[6]{#1~#2\vdash^{#3} #4 \leadsto #5 : #6}
\newcommand{\cvalidEP}[5]{#1 \vdash^{#2} #3 \leadsto #4 : #5}
\newcommand{\cvalidEPX}[3]{\cvalidEP{\Omega}{\escenev}{#1}{#2}{#3}}
\newcommand{\csyn}[6]{#1~#2 \vdash^{#3} #4 \leadsto #5 \Rightarrow #6}
\newcommand{\csynX}[3]{\csyn{\Delta}{\Gamma}{\escenev}{#1}{#2}{#3}}
\newcommand{\cana}[6]{#1~#2 \vdash^{#3} #4 \leadsto #5 \Leftarrow #6}
\newcommand{\canaX}[3]{\cana{\Delta}{\Gamma}{\escenev}{#1}{#2}{#3}}
\newcommand{\cvalidEX}[3]{\cvalidE{\Delta}{\Gamma}{\escenev}{#1}{#2}{#3}}
\newcommand{\escenev}{\mathbbmss{E}}
\newcommand{\tscenev}{\mathbbmss{T}}
\newcommand{\esceneU}[4]{#1;\,#2;\,#3;\,#4}
\newcommand{\esceneUP}[5]{#1;\,#2;\,#3;\,#4;\,#5}
\newcommand{\esceneSG}[5]{#1;\,#2;\,#3{\setlength{\fboxsep}{0pt}\colorbox{light-gray}{\fontsize{9pt}{0pt}\selectfont ;\,$#4$}};\,#5}
\newcommand{\esceneSGB}[5]{#1;\,#2;\,#3{\setlength{\fboxsep}{0pt}\colorbox{light-gray}{;\,$#4$}};\,#5}
\newcommand{\tsceneU}[2]{#1;\,#2}
\newcommand{\tsceneUP}[2]{\tsceneU{#1}{#2}}
\newcommand{\tsfrom}[1]{\mathsf{ts}(#1)}
\newcommand{\parseUTypF}[1]{\mathsf{parseUTyp}(#1)}
\newcommand{\parseUExpF}[1]{\mathsf{parseUExp}(#1)}
\newcommand{\parseUTyp}[2]{\mathsf{parseUTyp}(#1)=#2}
\newcommand{\parseUExp}[2]{\mathsf{parseUExp}(#1)=#2}
\newcommand{\bsubseq}[3]{\mathsf{subseq}(#1; #2; #3)}

\newcommand{\sizeof}[1]{\Vert #1 \Vert}

% Pattern matching
\newcommand{\matchwith}[2]{\texttt{match}~#1~#2}
\newcommand{\aematchwith}[3]{\abopi{match}{#1}{#2; #3}}
\newcommand{\aumatchwith}[4]{\abopic{umatch}{#1}{#2}{#3; #4}}
\newcommand{\acematchwith}[3]{\abopi{prmatch}{#1}{#2; #3}}

\newcommand{\aumatchwithb}[3]{\abopi{umatch}{#1}{#2; #3}}
\newcommand{\acematchwithb}[3]{\abopi{prmatch}{#1}{#2; #3}}

\newcommand{\matchrule}[2]{#1 \Rightarrow #2}
\newcommand{\aematchrule}[2]{\abop{rule}{#1.#2}}
\newcommand{\aumatchrule}[2]{\abop{urule}{#1.#2}}
\newcommand{\acematchrule}[2]{\abop{prrule}{#1.#2}}

\newcommand{\dashVx}{\text{\reflectbox{$\Vdash$}}}
\newcommand{\dashV}{~\dashVx~}
\newcommand{\ruleType}[5]{#1~#2 \vdash #3 : #4 \Mapsto #5}
\newcommand{\patType}[3]{\Delta \vdash #2 : #3 \dashV #1}
\newcommand{\patTypeD}[4]{#3 : #4 \dashV #2}
\newcommand{\ruleTypeP}[4]{#1 \vdash #2 : #3 \Mapsto #4}
\newcommand{\patTypeP}[3]{\Omega \vdash #2 : #3 \dashV #1}
\newcommand{\patTypePC}[4]{#1 \vdash #3 : #4 \dashV #2}
% \newcommand{\pctx}{\varUpsilon}
\newcommand{\pctx}{\Gamma}

\newcommand{\matchfail}[1]{#1~\mathsf{matchfail}}

\newcommand{\eR}{R}
\newcommand{\uR}{\hat{R}}
\newcommand{\cR}{\grave{R}}

\newcommand{\erv}{r}
\newcommand{\urv}{\hat{r}}
\newcommand{\crv}{\grave{r}}

\newcommand{\epv}{p}
\newcommand{\upv}{\hat{p}}
\newcommand{\cpv}{\grave{p}}

\newcommand{\wildp}{\_}
\newcommand{\aewildp}{\texttt{wildp}}
\newcommand{\auwildp}{\texttt{uwildp}}
\newcommand{\acewildp}{\texttt{prwildp}}

\newcommand{\foldtp}[2]{\texttt{fold}_{#1}(#2)}
\newcommand{\foldp}[1]{\abop{fold}{#1}}
\newcommand{\aefoldp}[1]{\abop{foldp}{#1}}
\newcommand{\aufoldp}[1]{\abop{ufoldp}{#1}}
\newcommand{\acefoldp}[1]{\abop{prfoldp}{#1}}

\newcommand{\tplpt}[2]{\langle #1 \rangle_{#2}}
\newcommand{\tplp}[1]{\langle #1 \rangle}
\newcommand{\aetplp}[2]{\abopi{tplp}{#1}{#2}}
\newcommand{\autplp}[2]{\abopi{utplp}{#1}{#2}}
\newcommand{\acetplp}[2]{\abopi{prtplp}{#1}{#2}}

\newcommand{\injtp}[3]{\texttt{inj}_{#1}~#2 \cdot #3}
\newcommand{\injp}[2]{\texttt{inj}[#1](#2)}
\newcommand{\aeinjp}[2]{\abopi{injp}{#1}{#2}}
\newcommand{\auinjp}[2]{\abopi{uinjp}{#1}{#2}}
\newcommand{\aceinjp}[2]{\abopi{prinjp}{#1}{#2}}

\newcommand{\usyntaxueP}[4]{\texttt{syntax}~#1~\texttt{at}~#2~\texttt{for expressions}~\{#3\}~\texttt{in}~#4}
\newcommand{\usyntaxup}[4]{\texttt{syntax}~#1~\texttt{at}~#2~\texttt{for}~\texttt{patterns}~\texttt{by}~\texttt{static}~#3~\texttt{in}~#4}
\newcommand{\audefuptsm}[4]{\abopcc{usyntaxsp}{#2}{#1}{#3.#4}}
\newcommand{\auapuptsm}[2]{\texttt{uapsptlm}[#1]\texttt{[}#2\texttt{]}}

\newcommand{\expandsUP}[7]{#1~#2 \vdash_{#3;\,#4} #5 \leadsto #6 : #7} % there's a multiline one in the document done manually
\newcommand{\expandsUPX}[3]{\expandsUP{\uDelta}{\uGamma}{\uPsi}{\uPhi}{#1}{#2}{#3}}

\newcommand{\expandsSG}[7]{#1~#2~{\vdash_{#3}}{\setlength{\fboxsep}{0px}\colorbox{light-gray}{$_{\mathstrut; #4}$}}~ #5 \leadsto #6 : #7}

\newcommand{\ruleExpands}[8]{#1~#2 \vdash_{#3;\,#4} #5 \leadsto #6 : #7 \Mapsto #8}
\newcommand{\patExpands}[5]{\uDelta \vdash_{#2} #3 \leadsto #4 : #5 \dashV #1}
\newcommand{\xuptsmdef}[2]{\abop{sptlm}{#1;\,#2}}
\newcommand{\xuptsmbnd}[3]{#1 \hookrightarrow \xuptsmdef{#2}{#3}}
\newcommand{\uptsmenv}[2]{#1 \vdash #2~\mathsf{spTLMs}}
\newcommand{\uptsmctx}[2]{#1 \vdash #2~\mathsf{spTLMctx}}

\newcommand{\tParseResultPat}{\mathtt{ParseResultSP}} 
\newcommand{\tCEPat}{\mathtt{PrPat}} % Typed expansion
\newcommand{\tPCEPat}{\mathtt{PPrPat}}

\newcommand{\decodeCEPat}[2]{#1 \uparrow_\mathsf{PrPat} #2}
\newcommand{\encodeCEPat}[2]{#1 \downarrow_\mathsf{PrPat} #2}
\newcommand{\decodePCEPat}[2]{#1 \uparrow_\mathsf{PPrPat} #2}
\newcommand{\encodePCEPat}[2]{#1 \downarrow_\mathsf{PPrPat} #2}


\newcommand{\cvalidP}[5]{#3 \leadsto #4 : #5~\dashVx^{#2}\,{#1}}
\newcommand{\cvalidR}[7]{#1~#2 \vdash^{#3} #4 \leadsto #5 : #6 \Mapsto #7}
\newcommand{\cvalidRP}[6]{#1 \vdash^{#2} #3 \leadsto #4 : #5 \Mapsto #6}
\newcommand{\crsyn}[7]{#1~#2 \vdash^{#3} #4 \leadsto #5 \Rightarrow #6 \Mapsto #7}
\newcommand{\crsynX}[4]{\crsyn{\Delta}{\Gamma}{\escenev}{#1}{#2}{#3}{#4}}
\newcommand{\crana}[7]{#1~#2 \vdash^{#3} #4 \leadsto #5 \Leftarrow #6 \Mapsto #7}
\newcommand{\cranaX}[4]{\crana{\Delta}{\Gamma}{\escenev}{#1}{#2}{#3}{#4}}
\newcommand{\pscenev}{\mathbbmss{P}}
\newcommand{\pscene}[3]{#1;\,#2;\,#3}

\newcommand{\parseURule}[2]{\mathsf{parseURule}(#1)=#2}
\newcommand{\parseUPat}[2]{\mathsf{parseUPat}(#1)=#2}
\newcommand{\parseUPatF}[1]{\mathsf{parseUPat}(#1)}


\newcommand{\uPhi}{\hat\Phi}
\newcommand{\uAP}[2]{\langle #1; #2 \rangle}
\newcommand{\upctx}{\hat\Gamma}

% Implicits
\newcommand{\implicite}[2]{\texttt{implicit\,syntax}~#1~\texttt{for\,expressions\,in}~#2}
\newcommand{\auimplicite}[2]{\abopp{uimplicite}{#1}{#2}}

\newcommand{\implicitp}[2]{\texttt{implicit\,syntax}~#1~\texttt{for\,patterns\,in}~#2}
\newcommand{\auimplicitp}[2]{\abopp{uimplicitp}{#1}{#2}}

\newcommand{\lit}[1]{{\texttt{/}#1\texttt{/}}}
\newcommand{\auelit}[1]{\abopbz{uelit}{#1}}
\newcommand{\auplit}[1]{\abopbz{uplit}{#1}}

\newcommand{\eana}[7]{#1~#2 \vdash_{#3; #4} #5 \leadsto #6 \Leftarrow #7}
\newcommand{\eanaX}[3]{\eana{\uDelta}{\uGamma}{\uPsi}{\uPhi}{#1}{#2}{#3}}
\newcommand{\esyn}[7]{#1~#2 \vdash_{#3; #4} #5 \leadsto #6 \Rightarrow #7}
\newcommand{\esynX}[3]{\esyn{\uDelta}{\uGamma}{\uPsi}{\uPhi}{#1}{#2}{#3}}
\newcommand{\rana}[8]{#1~#2 \vdash_{#3; #4} #5 \leadsto #6 \Leftarrow #7 \Mapsto #8}
\newcommand{\ranaX}[4]{\rana{\uDelta}{\uGamma}{\uPsi}{\uPhi}{#1}{#2}{#3}{#4}}
\newcommand{\rsyn}[8]{#1~#2 \vdash_{#3; #4} #5 \leadsto #6 \Rightarrow #7 \Mapsto #8}
\newcommand{\rsynX}[4]{\rsyn{\uDelta}{\uGamma}{\uPsi}{\uPhi}{#1}{#2}{#3}{#4}}

\newcommand{\uASI}[3]{\langle #1; #2; #3 \rangle}
\newcommand{\uI}{\mathcal{I}}
\newcommand{\designate}[2]{#1 \hookrightarrow #2}
\newcommand{\uIOK}[2]{#1 \vdash #2~\mathsf{designations}}


% Kinds
\newcommand{\kty}{\texttt{T}}
\newcommand{\akty}{\texttt{Type}}
\newcommand{\aukty}{\texttt{uType}}
\newcommand{\acekty}{\texttt{prType}}

\newcommand{\ksing}[1]{[\texttt{=}#1]}
\newcommand{\aksing}[1]{\abop{S}{#1}}
\newcommand{\auksing}[1]{\abop{uS}{#1}}
\newcommand{\aceksing}[1]{\abop{prS}{#1}}

\newcommand{\kdarr}[3]{(#1 :: #2) \rightarrow #3}
\newcommand{\akdarr}[3]{\abop{darr}{#1; #2.#3}}
\newcommand{\aukdarr}[3]{\abop{udarr}{#1; #2.#3}}
\newcommand{\acekdarr}[3]{\abop{prdarr}{#1; #2.#3}}

\newcommand{\kunit}{\llangle\rrangle}
\newcommand{\akunit}{\texttt{unit}}
\newcommand{\aukunit}{\texttt{uunit}}
\newcommand{\acekunit}{\texttt{prunit}}
\newcommand{\kone}{\mathsf{1}}

\newcommand{\dpitem}[3]{\mapitem{#1 \triangleright #2}{#3}}
\newcommand{\kdprod}[1]{\llangle #1 \rrangle}
\newcommand{\kdprodstd}{\kdprod{\{\dpitem{\ell_i}{u_i}{\kappa_i}\}_{1 \leq i \leq n}}}
\newcommand{\akdprod}[3]{\abopi{dprod}{#1; #2}{#3}}
\newcommand{\akdprodstd}{\akdprod{n}{\seqschemaX{\ell}}{\seqschemaijb{u}{\kappa}{i}{1}{n}{j}{1}{i}}}

\newcommand{\kdbprod}[3]{(#1 :: #2) \times #3}
\newcommand{\akdbprod}[3]{\abop{dprod}{#1; #2.#3}}
\newcommand{\aukdbprod}[3]{\abop{udprod}{#1; #2.#3}}
\newcommand{\acekdbprod}[3]{\abop{prdprod}{#1; #2.#3}}

\newcommand{\iskind}[2]{#1 \vdash #2~\mathsf{kind}}
\newcommand{\iskindX}[1]{\iskind{\Omega}{#1}}

\newcommand{\kequal}[3]{#1 \vdash #2 \equiv #3}
\newcommand{\kequalX}[2]{\kequal{\Omega}{#1}{#2}}

\newcommand{\ksub}[3]{#1 \vdash #2 <:: #3}
\newcommand{\ksubX}[2]{\ksub{\Omega}{#1}{#2}}

% Constructors
\newcommand{\casc}[2]{#1 :: #2}
\newcommand{\aucasc}[2]{\abopc{uasc}{#1}{#2}}
\newcommand{\acecasc}[2]{\abopc{prasc}{#1}{#2}}

\newcommand{\cabs}[2]{\lambda #1.#2}
\newcommand{\acabs}[2]{\abop{abs}{#1.#2}}
\newcommand{\aucabs}[2]{\abop{uabs}{#1.#2}}
\newcommand{\acecabs}[2]{\abop{prabs}{#1.#2}}

\newcommand{\capp}[2]{#1(#2)}
\newcommand{\acapp}[2]{\abop{app}{#1; #2}}
\newcommand{\aucapp}[2]{\abop{uapp}{#1; #2}}
\newcommand{\acecapp}[2]{\abop{prapp}{#1; #2}}

\newcommand{\ctriv}{\llangle\rrangle}
\newcommand{\actriv}{\texttt{triv}}
\newcommand{\auctriv}{\texttt{utriv}}
\newcommand{\acectriv}{\texttt{prtriv}}

\newcommand{\cpair}[2]{\llangle #1, #2 \rrangle}
\newcommand{\acpair}[2]{\abop{pair}{#1; #2}}
\newcommand{\aucpair}[2]{\abop{upair}{#1; #2}}
\newcommand{\acecpair}[2]{\abop{prpair}{#1; #2}}

\newcommand{\dtpl}[1]{\llangle #1 \rrangle}
\newcommand{\dtplX}{\dtpl{\{\dpitem{\ell_i}{u_i}{c_i}\}_{1 \leq i \leq n}}}
\newcommand{\adtpl}[3]{\abopi{dtpl}{#1; #2}{#3}}
\newcommand{\adtplX}{\adtpl{n}{\seqschemaX{\ell}}{\seqschemaijb{u}{c}{i}{1}{n}{j}{1}{i}}}

\newcommand{\cprl}[1]{#1 \cdot \texttt{l}}
\newcommand{\acprl}[1]{\abop{prl}{#1}}
\newcommand{\aucprl}[1]{\abop{uprl}{#1}}
\newcommand{\acecprl}[1]{\abop{prprl}{#1}}

\newcommand{\adprj}[2]{\abopp{prj}{#1}{#2}}

\newcommand{\cprr}[1]{#1 \cdot \texttt{r}}
\newcommand{\acprr}[1]{\abop{prr}{#1}}
\newcommand{\aucprr}[1]{\abop{uprr}{#1}}
\newcommand{\acecprr}[1]{\abop{prprr}{#1}}

\newcommand{\mcon}[1]{#1\cdot\texttt{c}}
\newcommand{\amcon}[1]{\abop{con}{#1}}
\newcommand{\aumcon}[1]{\abop{ucon}{#1}}
\newcommand{\acemcon}[1]{\abop{prcon}{#1}}

\newcommand{\mval}[1]{#1 \cdot \texttt{v}}
\newcommand{\amval}[1]{\abop{val}{#1}}
\newcommand{\aumval}[1]{\abop{uval}{#1}}
\newcommand{\acemval}[1]{\abop{prval}{#1}}

\newcommand{\haskind}[3]{#1 \vdash #2 :: #3}
\newcommand{\haskindX}[2]{\haskind{\Omega}{#1}{#2}}

\newcommand{\cequal}[4]{#1 \vdash #2 \equiv #3 :: #4}
\newcommand{\cequalX}[3]{\cequal{\Omega}{#1}{#2}{#3}}

% Modules and signatures
\newcommand{\signature}[3]{\llbracket #1 :: #2; #3 \rrbracket}
\newcommand{\asignature}[3]{\abopc{sig}{#1}{#2.#3}}
\newcommand{\ausignature}[3]{\abopc{usig}{#1}{#2.#3}}

\newcommand{\struct}[2]{\llbracket #1; #2 \rrbracket}
\newcommand{\astruct}[2]{\abop{struct}{#1; #2}}
\newcommand{\austruct}[2]{\abop{ustruct}{#1; #2}}

\newcommand{\seal}[2]{#1 \upharpoonleft #2}
\newcommand{\aseal}[2]{\abopc{seal}{#1}{#2}}
\newcommand{\auseal}[2]{\abopc{useal}{#1}{#2}}

\newcommand{\mletdecl}[4]{\texttt{let}~#1~\texttt{=}~#2~\texttt{in}~#3}
\newcommand{\umletdecl}[5]{#1~\texttt{let}~#2~\texttt{=}~#3~\texttt{in}~#4}
\newcommand{\mlet}[4]{(\texttt{let}~#1~\texttt{=}~#2~\texttt{in}~#3) : #4}
\newcommand{\staticphase}{\texttt{static}}
\newcommand{\standardphase}{\texttt{standard}}
\newcommand{\mletH}[5]{(#1~\texttt{let}~#2~\texttt{=}~#3~\texttt{in}~#4) : #5}
\newcommand{\amlet}[4]{\abopc{mlet}{#1}{#2; #3.#4}}
\newcommand{\aumlet}[4]{\abopc{umlet}{#1}{#2; #3.#4}}

\newcommand{\syntaxps}[6]{#1~\texttt{syntax}~#2~\texttt{at}~#3~\texttt{for}~#4~\texttt{by}~\texttt{static}~#5~\texttt{in}~#6}
\newcommand{\letsyntaxps}[5]{#1~\texttt{let}~\texttt{syntax}~#2~\texttt{for}~#3=#4~\texttt{in}~#5}

\newcommand{\tsmapp}[2]{\texttt{/}#1\mathtt{/}~#2}

\newcommand{\bindMod}[2]{#1.#2}
\newcommand{\bindTyp}[2]{#1.#2}

\newcommand{\issig}[2]{#1 \vdash #2~\mathsf{sig}}
\newcommand{\issigX}[1]{\issig{\Omega}{#1}}

\newcommand{\sigequal}[3]{#1 \vdash #2 \equiv #3}
\newcommand{\sigequalX}[2]{\sigequal{\Omega}{#1}{#2}}

\newcommand{\sigsub}[3]{#1 \vdash #2 <: #3}
\newcommand{\sigsubX}[2]{\sigsub{\Omega}{#1}{#2}}

\newcommand{\hassig}[3]{#1 \vdash #2 : #3}
\newcommand{\hassigX}[2]{\hassig{\Omega}{#1}{#2}}

\newcommand{\raiseerror}{\mathtt{error}}
\newcommand{\isvalue}[1]{#1~\mathsf{val}}
\newcommand{\iserr}[1]{#1~\mathsf{err}}
\newcommand{\ismval}[2]{#1 \vdash #2~\mathsf{mval}}
\newcommand{\ismvalX}[1]{\ismval{\Omega}{#1}}

\newcommand{\statphase}{\mathtt{static}}
\newcommand{\dynphase}{\mathtt{dynamic}}

\newcommand{\expsortq}{\mathtt{Exp}}
\newcommand{\patsortq}{\mathtt{Pat}}

% Parameterized TLMs
\newcommand{\urho}{{\hat\rho}}
\newcommand{\uepsilon}{{\hat\epsilon}}
\newcommand{\uX}{{\hat X}}

\newcommand{\defpetsm}[4]{\texttt{syntax}~#1~\texttt{at}~#2~\texttt{for}~\texttt{expressions}~\texttt{by}~\texttt{static}~#3~\texttt{in}~#4}
\newcommand{\defpptsm}[4]{\texttt{syntax}~#1~\texttt{at}~#2~\texttt{for}~\texttt{patterns}~\texttt{by}~\texttt{static}~#3~\texttt{in}~#4}

\newcommand{\defpetsmH}[5]{#1~\texttt{syntax}~#2~\texttt{at}~#3~\texttt{for}~\texttt{expressions}~\texttt{by}~\texttt{static}~#4~\texttt{in}~#5}
\newcommand{\defpptsmH}[5]{#1~\texttt{syntax}~#2~\texttt{at}~#3~\texttt{for}~\texttt{patterns}~\texttt{by}~\texttt{static}~#4~\texttt{in}~#5}

\newcommand{\audefpetsm}[4]{\abopcc{usyntaxpe}{#2}{#1}{#3.#4}}
\newcommand{\aumdefpetsm}[4]{\abopcc{umsyntaxpe}{#2}{#1}{#3.#4}}
\newcommand{\auappetsm}[2]{\abopicz{uappetlm}{#1}{#2}}
\newcommand{\uletpetsm}[3]{\texttt{let}~\texttt{syntax}~#1=#2~\texttt{for}~\texttt{expressions}~\texttt{in}~#3}
\newcommand{\auletpetsm}[3]{\abopc{uletpetlm}{#1}{#2.#3}}
\newcommand{\aumletpetsm}[3]{\abopc{umletpetlm}{#1}{#2.#3}}

\newcommand{\uletpetsmH}[4]{#1~\texttt{let}~\texttt{syntax}~#2=#3~\texttt{for}~\texttt{expressions}~\texttt{in}~#4}

\newcommand{\audefpptsm}[4]{\abopcc{usyntaxpp}{#2}{#1}{#3.#4}}
\newcommand{\aumdefpptsm}[4]{\abopcc{umsyntaxpp}{#2}{#1}{#3.#4}}
\newcommand{\auappptsm}[2]{\abopicz{uappptlm}{#1}{#2}}
\newcommand{\uletpptsm}[3]{\texttt{let}~\texttt{syntax}~#1=#2~\texttt{for}~\texttt{patterns}~\texttt{in}~#3}

\newcommand{\uletpptsmH}[4]{#1~\texttt{let}~\texttt{syntax}~#2=#3~\texttt{for}~\texttt{patterns}~\texttt{in}~#4}

\newcommand{\auletpptsm}[3]{\abopc{uletpptlm}{#1}{#2.#3}}
\newcommand{\aumletpptsm}[3]{\abopc{umletpptlm}{#1}{#2.#3}}

\newcommand{\aetype}[1]{\abop{type}{#1}}
\newcommand{\autype}[1]{\abop{utype}{#1}}

\newcommand{\alltypes}[2]{\forall #1.#2}
\newcommand{\aealltypes}[2]{\abop{alltypes}{#1.#2}}
\newcommand{\aualltypes}[2]{\abop{ualltypes}{#1.#2}}

\newcommand{\allmods}[3]{\forall #1{:}#2.#3}
\newcommand{\aeallmods}[3]{\abopc{allmods}{#1}{#2.#3}}
\newcommand{\auallmods}[3]{\abopc{uallmods}{#1}{#2.#3}}

% \newcommand{\typeparam}[2]{\Lambda #1.#2}
% \newcommand{\aetypeparam}[2]{\abop{typeparam}{#1.#2}}
% \newcommand{\autypeparam}[2]{\abop{utypeparam}{#1.#2}}

% \newcommand{\modparam}[3]{\Lambda #1{:}#2.#3}
% \newcommand{\aemodparam}[3]{\abopc{modparam}{#1}{#2.#3}}
% \newcommand{\aumodparam}[3]{\abopc{umodparam}{#1}{#2.#3}}

\newcommand{\aptype}[2]{#1(#2)}
\newcommand{\aeaptype}[2]{\abopc{aptype}{#1}{#2}}
\newcommand{\auaptype}[2]{\abopc{uaptype}{#1}{#2}}

\newcommand{\apmod}[2]{#1(#2)}
\newcommand{\aeapmod}[2]{\abopc{apmod}{#1}{#2}}
\newcommand{\auapmod}[2]{\abopc{uapmod}{#1}{#2}}

\newcommand{\adefref}[1]{\aboppz{defref}{#1}}
\newcommand{\abindref}[1]{\aboppz{bindref}{#1}}

\newcommand{\uOmega}{{\hat\Omega}}

\newcommand{\kExpandsSP}[3]{#1 \vdash #2 \leadsto #3~\mathsf{kind}}
\newcommand{\kExpands}[3]{#1 \vdash #2 \leadsto #3~\mathsf{kind}}
\newcommand{\kExpandsX}[2]{\kExpands{\uOmega}{#1}{#2}}

\newcommand{\cExpandsSP}[4]{#1 \vdash #2 \leadsto #3 :: #4}

\newcommand{\kana}[4]{#1 \vdash #2 \leadsto #3 \Leftarrow #4}
\newcommand{\kanaX}[3]{\kana{\uOmega}{#1}{#2}{#3}}
\newcommand{\ksyn}[4]{#1 \vdash #2 \leadsto #3 \Rightarrow #4}
\newcommand{\ksynX}[3]{\ksyn{\uOmega}{#1}{#2}{#3}}

\newcommand{\cExpands}[4]{#1 \vdash #2 \leadsto #3 :: #4}
\newcommand{\cExpandsX}[3]{\cExpands{\uOmega}{#1}{#2}{#3}}

\newcommand{\eExpandsSP}[6]{#1 \vdash_{#2;#3} #4 \leadsto #5 : #6}

\newcommand{\eanaP}[6]{#1 \vdash_{#2; #3} #4 \leadsto #5 \Leftarrow #6}
\newcommand{\eanaPX}[3]{\eanaP{\uOmega}{\uPsi}{\uPhi}{#1}{#2}{#3}}
\newcommand{\esynP}[6]{#1 \vdash_{#2; #3} #4 \leadsto #5 \Rightarrow #6}
\newcommand{\esynPX}[3]{\esynP{\uOmega}{\uPsi}{\uPhi}{#1}{#2}{#3}}

\newcommand{\rExpandsSP}[7]{#1 \vdash_{#2; #3} #4 \leadsto #5 : #6 \Mapsto #7}
\newcommand{\ranaP}[7]{#1 \vdash_{#2; #3} #4 \leadsto #5 \Leftarrow #6 \Mapsto #7}
\newcommand{\ranaPX}[4]{\ranaP{\uOmega}{\uPsi}{\uPhi}{#1}{#2}{#3}{#4}}
\newcommand{\rsynP}[7]{#1 \vdash_{#2; #3} #4 \leadsto #5 \Rightarrow #6 \Mapsto #7}
\newcommand{\rsynPX}[4]{\rsynP{\uOmega}{\uPsi}{\uPhi}{#1}{#2}{#3}{#4}}

\newcommand{\pExpandsSP}[6]{#1 \vdash_{#2} #3 \leadsto #4 : #5 \dashV #6}
\newcommand{\patExpandsP}[5]{\uOmega \vdash_{#2} #3 \leadsto #4 : #5 \dashV #1}

\newcommand{\uKhyp}[3]{#1 \leadsto #2 :: #3}
\newcommand{\uMhyp}[3]{#1 \leadsto #2 : #3}

\newcommand{\uOmegaEx}[4]{\langle #3; #1; #2; #4 \rangle}
\newcommand{\uMctx}{\mathcal{M}}

\newcommand{\istypeP}[2]{\istypeU{#1}{#2}}
\newcommand{\istypePX}[1]{\istypeP{\Omega}{#1}}

\newcommand{\issubtypeP}[3]{#1 \vdash #2 <: #3}
\newcommand{\issubtypePX}[2]{\issubtypeP{\Omega}{#1}{#2}}

\newcommand{\tequalP}[3]{#1 \vdash #2 \equiv #3~\mathsf{type}}
\newcommand{\tequalPX}[2]{\tequalP{\Omega}{#1}{#2}}

\newcommand{\tExpandsP}[3]{#1 \vdash #2 \leadsto #3~\mathsf{type}}
\newcommand{\tExpandsPX}[2]{\tExpandsP{\uOmega}{#1}{#2}}


\newcommand{\sigExpandsSP}[3]{#1 \vdash #2 \leadsto #3~\mathsf{sig}}

\newcommand{\sigExpandsP}[3]{#1 \vdash #2 \leadsto #3~\mathsf{sig}}
\newcommand{\sigExpandsPX}[2]{\sigExpandsP{\uOmega}{#1}{#2}}

\newcommand{\uSigma}{{\hat\Sigma}}

\newcommand{\uPsiE}{\uPsi_\text{E}}
\newcommand{\uPsiP}{\uPsi_\text{P}}

\newcommand{\mExpandsSP}[7]{#1 \sslash #2 \vdash_{#3; #4} #5 \leadsto #6 : #7}

\newcommand{\msyn}[6]{#1 \vdash_{#2; #3} #4 \leadsto #5 \Rightarrow #6}
\newcommand{\msynX}[3]{\msyn{\uOmega}{\uPsi}{\uPhi}{#1}{#2}{#3}}
\newcommand{\mana}[6]{#1 \vdash_{#2; #3} #4 \leadsto #5 \Leftarrow #6}
\newcommand{\manaX}[3]{\mana{\uOmega}{\uPsi}{\uPhi}{#1}{#2}{#3}}

\newcommand{\mExpandsP}[6]{#1 \vdash_{#2; #3} #4 \leadsto #5 : #6}
\newcommand{\mExpandsPX}[3]{\mExpandsP{\uOmega}{\uPsi}{\uPhi}{#1}{#2}{#3}}

\newcommand{\mExpandsPH}[7]{#1 \vdash_{#2; #3}^{#7} #4 \leadsto #5 : #6}
\newcommand{\mExpandsPHX}[3]{\mExpandsPH{\uOmega}{\uPsi}{\uPhi}{#1}{#2}{#3}{\staticenvv}}

\newcommand{\staticenvv}{\Sigma}
\newcommand{\staticenv}[4]{#1 : #2; #3; #4}


\newcommand{\petsmdefn}[3]{#1 \hookrightarrow \texttt{petlm}(#2; #3)}
\newcommand{\pptsmdefn}[3]{#1 \hookrightarrow \texttt{pptlm}(#2; #3)}

\newcommand{\istsmty}[2]{#1 \vdash #2~\mathsf{tlmty}}
\newcommand{\tsmtyExpands}[3]{#1 \vdash #2 \leadsto #3 ~\mathsf{tlmty}}

\newcommand{\tParseResultPCEExp}{\mathtt{ParseResult}(\mathtt{PPrExpr})}
\newcommand{\tPProtoExpr}{\mathtt{PPrExpr}}

\newcommand{\tsmexpExpandsExp}[5]{#1 \vdash_{#2}^{\mathsf{Exp}} #3 \leadsto #4~@~#5}
\newcommand{\tsmexpExpandsExpX}[3]{\tsmexpExpandsExp{\Omega}{\uPsi}{#1}{#2}{#3}}

\newcommand{\tsmexpExpandsPat}[5]{#1 \vdash_{#2}^{\mathsf{Pat}} #3 \leadsto #4~@~#5}
\newcommand{\tsmexpExpandsPatX}[3]{\tsmexpExpandsPat{\Omega}{\uPsi}{#1}{#2}{#3}}

\newcommand{\hastsmtypeExp}[4]{#1 \vdash_{#2}^{\mathsf{Exp}} #3 ~@~ #4}
\newcommand{\hastsmtypePat}[4]{#1 \vdash_{#2}^{\mathsf{Pat}} #3 ~@~ #4}

\newcommand{\tsmexpNormalExp}[3]{#1 \vdash_{#2}^\mathsf{Exp} #3~\mathsf{normal}}
\newcommand{\tsmexpStepsExp}[4]{#1 \vdash_{#2}^\mathsf{Exp} #3 \mapsto #4}
\newcommand{\tsmexpMultistepsExp}[4]{#1 \vdash_{#2}^\mathsf{Exp} #3 \mapsto^{*} #4}
\newcommand{\tsmexpEvalsExp}[4]{#1 \vdash_{#2}^\mathsf{Exp} #3 \Downarrow #4}

\newcommand{\tsmexpNormalPat}[3]{#1 \vdash_{#2}^\mathsf{Pat} #3~\mathsf{normal}}
\newcommand{\tsmexpStepsPat}[4]{#1 \vdash_{#2}^\mathsf{Pat} #3 \mapsto #4}
\newcommand{\tsmexpMultistepsPat}[4]{#1 \vdash_{#2}^\mathsf{Pat} #3 \mapsto^{*} #4}
\newcommand{\tsmexpEvalsPat}[4]{#1 \vdash_{#2}^\mathsf{Pat} #3 \Downarrow #4}


\newcommand{\tsmdefof}[1]{\mathsf{tlmdef}(#1)}

\newcommand{\decodePCEExp}[2]{#1 \uparrow_\mathsf{PPrExpr} #2}
\newcommand{\encodePCEExp}[2]{#1 \downarrow_\mathsf{PPrExpr} #2}

\newcommand{\pce}{\dot{e}}
\newcommand{\pcp}{\dot{p}}

\newcommand{\prepce}[8]{#1 \vdash_{#2}^\mathsf{Exp} #3 \looparrowright_{#5} #4 ~?~ #6 \dashv #7 : #8}
\newcommand{\prepcp}[8]{#1 \vdash_{#2}^\mathsf{Pat} #3 \looparrowright_{#5} #4 ~?~ #6 \dashv #7 : #8}

%\newcommand{\cvalidT}[4]{#1\vdash^{#2} #3 \leadsto #4~\mathsf{type}}
% \newcommand{\cvalidE}[6]{#1~#2\vdash^{#3} #4 \leadsto #5 : #6}
\newcommand{\csynP}[5]{#1 \vdash^{#2} #3 \leadsto #4 \Rightarrow #5}
\newcommand{\csynPX}[3]{\csynP{\Omega}{\escenev}{#1}{#2}{#3}}
\newcommand{\canaP}[5]{#1 \vdash^{#2} #3 \leadsto #4 \Leftarrow #5}
\newcommand{\canaPX}[3]{\canaP{\Omega}{\escenev}{#1}{#2}{#3}}
%\newcommand{\cvalidEX}[3]{\cvalidE{\Delta}{\Gamma}{\escenev}{#1}{#2}{#3}}
%\newcommand{\escenev}{\mathbbmss{E}}
%\newcommand{\tscenev}{\mathbbmss{T}}
\newcommand{\esceneP}[5]{#1;\,#2;\,#3;\,#4;\,#5}
\newcommand{\tsceneP}[2]{\tsceneU{#1}{#2}}
\newcommand{\psceneP}[4]{#1;\,#2;\,#3;\,#4}

\newcommand{\abstype}[2]{\Lambda #1.#2}
\newcommand{\aeabstype}[2]{\abop{abstype}{#1.#2}}
\newcommand{\auabstype}[2]{\abop{uabstype}{#1.#2}}

\newcommand{\absmod}[3]{\Lambda #1{:}#2.#3}
\newcommand{\aeabsmod}[3]{\abopc{absmod}{#1}{#2.#3}}
\newcommand{\auabsmod}[3]{\abopc{uabsmod}{#1}{#2.#3}}

\newcommand{\tsmapparam}[2]{#1(#2)}

\newcommand{\pcebindtype}[2]{\Lambda #1.#2}
\newcommand{\apcebindtype}[2]{\abop{prbindtype}{#1.#2}}

\newcommand{\pcebindmod}[2]{\Lambda #1.#2}
\newcommand{\apcebindmod}[2]{\abop{prbindmod}{#1.#2}}

\newcommand{\pceexp}[1]{#1}
\newcommand{\apceexp}[1]{\abop{prexp}{#1}}
\newcommand{\apcepat}[1]{\abop{prpat}{#1}}

\newcommand{\cekappa}{{\grave\kappa}}
\newcommand{\cec}{{\grave c}}

\newcommand{\tParseResultCEPat}{\mathtt{ParseResult}(\mathtt{PPrPat})}

\newcommand{\cscenev}{\mathbbmss{C}}
\newcommand{\csceneP}[3]{#1;\,#2;\,#3}
\newcommand{\OParams}{\Omega_\text{params}}

\newcommand{\cvalidK}[4]{#1 \vdash^{#2} #3 \leadsto #4~\mathsf{kind}}
\newcommand{\cvalidKX}[2]{\cvalidK{\Omega}{\cscenev}{#1}{#2}}

\newcommand{\cvalidC}[5]{#1 \vdash^{#2} #3 \leadsto #4 :: #5}
\newcommand{\cvalidCX}[3]{\cvalidC{\Omega}{\cscenev}{#1}{#2}{#3}}
\newcommand{\ccsyn}[5]{#1 \vdash^{#2} #3 \leadsto #4 \Rightarrow #5}
\newcommand{\ccsynX}[3]{\ccsyn{\Omega}{\cscenev}{#1}{#2}{#3}}
\newcommand{\ccana}[5]{#1 \vdash^{#2} #3 \leadsto #4 \Leftarrow #5}
\newcommand{\ccanaX}[3]{\ccana{\Omega}{\cscenev}{#1}{#2}{#3}}

% \newcommand{\cvalidR}[6]{#1 \vdash^{#2} #3 \leadsto #4 : #5 \Mapsto #6}
% \newcommand{\cvalidRX}[4]{\cvalidR{\Omega}{\escenev}{#1}{#2}{#3}{#4}}
\newcommand{\crsynP}[6]{#1 \vdash^{#2} #3 \leadsto #4 \Rightarrow #5 \Mapsto #6}
\newcommand{\crsynPX}[4]{\crsynP{\Omega}{\escenev}{#1}{#2}{#3}{#4}}
\newcommand{\cranaP}[6]{#1 \vdash^{#2} #3 \leadsto #4 \Leftarrow #5 \Mapsto #6}
\newcommand{\cranaPX}[4]{\cranaP{\Omega}{\escenev}{#1}{#2}{#3}{#4}}

\newcommand{\parseUMod}[2]{\mathsf{parseUMod}(#1)=#2}
\newcommand{\parseUModF}[1]{\mathsf{parseUMod}(#1)}
\newcommand{\parseUSigF}[1]{\mathsf{parseUSig}(#1)}
\newcommand{\parseUSig}[2]{\mathsf{parseUSig}(#1)=#2}
\newcommand{\parseUKind}[2]{\mathsf{parseUKind}(#1)=#2}
\newcommand{\parseUKindF}[1]{\mathsf{parseUKind}(#1)}
\newcommand{\parseUConF}[1]{\mathsf{parseUCon}(#1)}
\newcommand{\parseUCon}[2]{\mathsf{parseUCon}(#1)=#2}

\newcommand{\cvalidTP}[4]{#1 \vdash^{#2} #3 \leadsto #4~\mathsf{type}}

\newcommand{\csfrom}[1]{\mathsf{cs}(#1)}

\newcommand{\cvalidPPE}[5]{#3 \leadsto #4 : #5~\dashVx^{#2}{\,#1}}
\newcommand{\cvalidPP}[5]{#3 \leadsto #4 : #5~\dashVx^{#2}{\,#1}}

\newcommand{\isvalP}[1]{#1~\mathsf{val}}

\newcommand{\suc}[1]{\abop{s}{#1}}
\newcommand{\asuc}[1]{\abop{succ}{#1}}

\newcommand{\zero}{\texttt{z}}
\newcommand{\azero}{\texttt{zero}}

\newcommand{\defeq}{\mathrel{\overset{\makebox[0pt]{\mbox{\normalfont\scriptsize def}}}{=}}}

\newcommand{\graybox}[1]{\setlength{\fboxsep}{1.5pt}\colorbox{light-gray}{\vphantom{]}$#1$}}
\newcommand{\yellowbox}[1]{\setlength{\fboxsep}{1.5pt}\colorbox{Yellow}{\vphantom{]}$#1$}}

\newcommand{\graytxtbox}[1]{\setlength{\fboxsep}{1.5pt}\colorbox{light-gray}{\vphantom{]}#1}}

\newmdenv[backgroundcolor=light-gray,hidealllines=true,innerleftmargin=1pt,innerrightmargin=1pt,leftmargin=0pt,rightmargin=0pt,innertopmargin=1.5pt,innerbottommargin=1.5pt]{grayparbox}


\newcommand{\uDOK}[1]{\vdash #1~\mathsf{utctx}}

\newcommand{\segof}[1]{\mathsf{seg}(#1)}
\newcommand{\segOK}[2]{#1~\mathsf{segments}~#2}
\newcommand{\segOKP}[4]{#1 \vdash^{#2} \segOK{#3}{#4}}
\newcommand{\segExp}[2]{\langle #1; #2; \mathsf{UExp} \rangle}
\newcommand{\segTyp}[2]{\langle #1; #2; \mathsf{UTyp} \rangle}
\newcommand{\segPat}[2]{\langle #1; #2; \mathsf{UPat}\rangle}
\newcommand{\segCon}[2]{\langle #1; #2; \mathsf{UCon}\rangle}
\newcommand{\segKind}[2]{\langle #1; #2; \mathsf{UKind} \rangle}

% \newcommand{\summaryOf}[1]{\mathsf{summary}(#1)}

\newcommand{\nty}{n_\text{ty}}
\newcommand{\ntyj}{n_\text{ty,$j$}}
\newcommand{\nexp}{n_\text{exp}}
\newcommand{\nexpj}{n_\text{exp,$j$}}
\newcommand{\nrules}{n}
\newcommand{\npat}{n_\text{pat}}
\newcommand{\npatj}{n_\text{pat,$j$}}
\newcommand{\nkind}{n_\text{kind}}
\newcommand{\ncon}{n_\text{con}}

\newcommand{\fvof}[1]{\mathsf{fv}(#1)}