\newcommand{\FV}[1]{\mathrm{FV}(#1)}

\newcommand{\alt}{\mathrel{|}}

\newcommand{\MinML}{\mbox{\textsf{MinML}}}
\newcommand{\Integer}{\mathcd{int}}
\newcommand{\Boolean}{\mathcd{bool}}
\newcommand{\Float}{\mathcd{float}}
\newcommand{\Function}[2]{{#1}\,{\to}\,{#2}}
\newcommand{\Times}[2]{{#1}\,{\times}\,{#2}}
\newcommand{\Plus}[2]{{#1}\,{+}\,{#2}}

\newcommand{\mathcd}[1]{\textbf{#1}}
\newcommand{\Numeral}[1]{#1}
\newcommand{\True}{\mathcd{true}}
\newcommand{\False}{\mathcd{false}}
\newcommand{\PrimOp}[2]{{#1}({#2})}
\newcommand{\cdparens}[1]{\mathcd{(}{#1}\mathcd{)}}
\newcommand{\Fun}[3]{\mathcd{fun}\;{#1}\cdparens{#2}\;\mathcd{is}\;{#3}\;\mathcd{end}}
\newcommand{\FunT}[5]{\mathcd{fun}\;{#1}\cdparens{{#2}\mathcd{:}{#3}}\mathcd{:}{#4}\;\mathcd{is}\;{#5}\;\mathcd{end}}
\newcommand{\FunwithA}[5]{\mathcd{fun}\;{#1}\cdparens{{#2}\mathcd{:}{#3}}\mathcd{:}{#4}\;\mathcd{is}\;{#5}\;}
\newcommand{\FunwithB}[5]{\mathcd{with}\;{#1}\cdparens{{#2}\mathcd{:}{#3}}\mathcd{:}{#4}\;\mathcd{is}\;{#5}\;\mathcd{end}}
\newcommand{\Apply}[2]{\mathcd{apply}\cdparens{{#1},{#2}}}
\newcommand{\Pair}[2]{\cdparens{{#1},{#2}}}
\newcommand{\Bind}[3]{\mathcd{bind}\;{#1}\;\mathcd{to}\;{#2}\;\mathcd{in}\;{#3}}
\newcommand{\Inleft}[1]{\mathcd{inl}\;{#1}}
\newcommand{\Inright}[1]{\mathcd{inr}\;{#1}}
\newcommand{\Case}[5]{\mathcd{case}\;{#1}\;\mathcd{of}\;\Inleft{#2}\;\mathcd{=>}\;{#3}\;\mathcd{|}\;\Inright{#4}\;\mathcd{=>}\;{#5}}
\newcommand{\InleftT}[3]{\mathcd{inl}_{{#1}+{#2}}\;{#3}}
\newcommand{\InrightT}[3]{\mathcd{inr}_{{#1}+{#2}}\;{#3}}
\newcommand{\CaseT}[7]{\mathcd{case}\;{#1}\;\mathcd{of}\;\Inleft{#2}:{#3}\;\mathcd{=>}\;{#4}\;\mathcd{|}\;\Inright{#5}:{#6}\;\mathcd{=>}\;{#7}}

\newcommand{\WildPat}{{\tt \bf \_}}
\newcommand{\VarPat}[2]{{#1}:{#2}}

\newcommand{\TVar}{\mbox{[\textbf{VarTyp}]}}
\newcommand{\TNum}{\mbox{[\textbf{NumTyp}]}}
\newcommand{\TInt}{\mbox{[\textbf{IntTyp}]}}
\newcommand{\TFloat}{\mbox{[\textbf{FloatTyp}]}}
\newcommand{\TTrue}{\mbox{[\textbf{TrueTyp}]}}
\newcommand{\TFalse}{\mbox{[\textbf{FalseTyp}]}}
\newcommand{\TOp}{\mbox{[\textbf{OpTyp}]}}
\newcommand{\TIf}{\mbox{[\textbf{IfTyp}]}}
\newcommand{\TFun}{\mbox{[\textbf{FunTyp}]}}
\newcommand{\TApp}{\mbox{[\textbf{AppTyp}]}}
\newcommand{\TPair}{\mbox{[\textbf{PairTyp}]}}
\newcommand{\TBind}{\mbox{[\textbf{BindTyp}]}}
\newcommand{\TInl}{\mbox{[\textbf{InlTyp}]}}
\newcommand{\TInr}{\mbox{[\textbf{InrTyp}]}}
\newcommand{\TCase}{\mbox{[\textbf{CaseTyp}]}}
\newcommand{\TSub}{\mbox{[\textbf{Subsume}]}}

\newcommand{\PWild}{\mbox{[\textbf{WildPat}]}}
\newcommand{\PVar}{\mbox{[\textbf{VarPat}]}}
\newcommand{\PPair}{\mbox{[\textbf{PairPat}]}}

\newcommand{\StepsTo}{\mathrel{\mapsto}}

\newcommand{\IOp}{\mbox{[\textbf{OpVals}]}}
\newcommand{\IIfT}{\mbox{[\textbf{IfTrue}]}}
\newcommand{\IIfF}{\mbox{[\textbf{IfFalse}]}}
\newcommand{\IApp}{\mbox{[\textbf{AppFun}]}}
\newcommand{\IBindW}{\mbox{[\textbf{BindWild}]}}
\newcommand{\IBindV}{\mbox{[\textbf{BindVar}]}}
\newcommand{\IBindP}{\mbox{[\textbf{BindPair}]}}
\newcommand{\ICaseL}{\mbox{[\textbf{CaseLeft}]}}
\newcommand{\ICaseR}{\mbox{[\textbf{CaseRight}]}}
\newcommand{\EOp}[1]{\mbox{$[\mathbf{OpArg}_{#1}]$}}
\newcommand{\EIf}{\mbox{[\textbf{IfTest}]}}
\newcommand{\EAppF}{\mbox{[\textbf{AppFun}]}}
\newcommand{\EAppA}{\mbox{[\textbf{AppArg}]}}
\newcommand{\EPairL}{\mbox{[\textbf{PairLeft}]}}
\newcommand{\EPairR}{\mbox{[\textbf{PairRight}]}}
\newcommand{\EBind}{\mbox{[\textbf{BindRhs}]}}
\newcommand{\EInl}{\mbox{[\textbf{InlArg}]}}
\newcommand{\EInr}{\mbox{[\textbf{InrArg}]}}
\newcommand{\ECase}{\mbox{[\textbf{CaseTest}]}}




\newcommand{\LetBe}[4]{\mathtt{let}\;{#2}{:}{#1}\;\mathtt{be}\;{#3}\;\mathtt{in}\;{#4}\;\mathtt{end}}

\newcommand{\gens}{\mathrel{\hookrightarrow}}

\newcommand{\DefProg}[2]{\mathcd{def}\;{#1}\;\mathcd{=}\;{#2}}
\newcommand{\EvalProg}[1]{\mathcd{eval}\;{#1}}
\newcommand{\QuitProg}{\mathcd{quit}}

\newcommand{\typingJ}[3]{{#1}\vdash{#2}:{#3}}
\newcommand{\stepsJ}[2]{{#1}\StepsTo{#2}}
\newcommand{\stepsbrJ}[2]
{\begin{array}{c}
{#1}\StepsTo \\
{#2}
\end{array}}
\newcommand{\typpatJ}[4]{{#1}\vdash{#2}:{#3}\gens{#4}}
\newcommand{\cgenJ}[5]{{#1}\vdash{#2}\leadsto_C{#3}:{#4}\,[{#5}]}
\newcommand{\cgenbrJ}[5]
{\begin{array}{c}
{#1}\vdash{#2}\leadsto_C \\ {#3}:{#4}\,[{#5}]
\end{array}}
\newcommand{\cgenpatJ}[5]{{#1}\vdash{#2}\leadsto_C({#3},{#4},{#5})}

\newcommand{\hole}{\square}
\newcommand{\cons}{\triangleright}
\newcommand{\Cstep}{\StepsTo_{\sf C}}

\newcommand{\minml}{{\sf MinML}}
\newcommand{\rulen}[1]{[\textbf{#1}]}
\newcommand{\nl}{\mbox{}}
\newcommand{\subtype}{\ \mathcd{<:}\ }
\newcommand{\computes}{\Rightarrow}
\newcommand{\lub}{\mbox{\textbf{lub}}}
\newcommand{\glb}{\mbox{\textbf{glb}}}
