\newcommand{\tmhastype}[2]{#1 : #2}
\newcommand{\Steps}{\mathrel{\,\longrightarrow\,}}

\newcommand{\sn}[2]{#1 \vdash #2 \in \ensuremath{\mathsf{sn}}}
\newcommand{\csn}[2]{#1 \vdash #2 \in \ensuremath{\mathsf{SN}}}

\newcommand{\app}{\;}
\newcommand{\rcs}[3]{\ensuremath{#1 \vdash #2\in \mathcal{R}_{#3} }}
\def\hastype{\mathrel{:}}
% ---------------------------------------------------------------------------- %
% -------------------------- Inference rules' names -------------------------- %
% ---------------------------------------------------------------------------- %

\newcommand{\ruleName}[1]{\textsc{\footnotesize #1}\xspace}

\newcommand {\TIf}           {\ruleName{T-If}}
\newcommand {\TPred}         {\ruleName{T-Pred}}
\newcommand {\TSucc}         {\ruleName{T-Succ}}
\newcommand {\TZero}         {\ruleName{T-Zero}}
\newcommand {\TIsZero}       {\ruleName{T-Iszero}}
\newcommand {\TPlus}         {\ruleName{T-Plus}}
\newcommand {\TMult}         {\ruleName{T-Mult}}
\newcommand {\TEq}           {\ruleName{T-Eq}}
\newcommand {\TApp}          {\ruleName{T-App}}
\newcommand {\TLam}          {\ruleName{T-Lam}}
\newcommand {\TAbs}          {\ruleName{T-Abs}}
\newcommand {\TSub}          {\ruleName{T-Sub}}
\newcommand {\TFn}           {\ruleName{T-Abs}}
\newcommand {\TFun}          {\ruleName{T-Fun}}
\newcommand {\TPair}         {\ruleName{T-Pair}}
\newcommand {\TFst}          {\ruleName{T-Fst}}
\newcommand {\TSnd}          {\ruleName{T-Snd}}
\newcommand {\TVar}          {\ruleName{T-Var}}
\newcommand {\TNum}          {\ruleName{T-Num}}
\newcommand {\TTrue}         {\ruleName{T-True}}
\newcommand {\TFalse}        {\ruleName{T-False}}
\newcommand {\TBase}         {\ruleName{T-Base}}

\newcommand {\TBinaryPrimop} {\ruleName{T-Binary-Primop}}
\newcommand {\TUnaryPrimop}  {\ruleName{T-Unary-Primop}}
\newcommand {\TTuple}        {\ruleName{T-Tuple}}
\newcommand {\TTupleSyn}     {\ruleName{T-Tuple-Syn}}
\newcommand {\TRec}          {\ruleName{T-Rec}}
\newcommand {\TAnno}         {\ruleName{T-Anno}}

\newcommand {\TrLam}         {\ruleName{Tr-Lam}}
\newcommand {\TrApp}         {\ruleName{Tr-App}}
\newcommand {\TrTop}         {\ruleName{Tr-Top}}
\newcommand {\TrNext}        {\ruleName{Tr-Next}}

\newcommand {\TLet}          {\ruleName{T-Let}}
\newcommand {\TLetSyn}       {\ruleName{T-Let-Syn}}
\newcommand {\TDecs}         {\ruleName{T-Decs}}
\newcommand {\TByName}       {\ruleName{T-By-Name}}
\newcommand {\TByVal}        {\ruleName{T-By-Val}}
\newcommand {\TByValTuple}   {\ruleName{T-By-Val-Tuple}}

\newcommand {\EIfTrue}       {\ruleName{E-IfTrue}}
\newcommand {\EIfT}          {\EIfTrue}                          % to be deleted
\newcommand {\EIfFalse}      {\ruleName{E-IfFalse}}
\newcommand {\EIfF}          {\EIfFalse}                         % to be deleted
\newcommand {\EIf}           {\ruleName{E-If}}
\newcommand {\ESucc}         {\ruleName{E-Succ}}
\newcommand {\ESuc}          {\ESucc}                            % to be deleted
\newcommand {\EPred}         {\ruleName{E-Pred}}
\newcommand {\EPredZero}     {\ruleName{E-PredZero}}
\newcommand {\EPredZ}        {\EPredZero}                        % to be deleted
\newcommand {\EPredSucc}     {\ruleName{E-PredSucc}}
\newcommand {\EIszero}       {\ruleName{E-Iszero}}
\newcommand {\EIsZero}       {\EIszero}                          % to be deleted
\newcommand {\EIszeroZero}   {\ruleName{E-IszeroZero}}
\newcommand {\EIsZeroZ}      {\EIszeroZero}                      % to be deleted
\newcommand {\EIszeroSucc}   {\ruleName{E-IszeroSucc}}
\newcommand {\EIsZeroSucc}   {\EIszeroSucc}                      % to be deleted

\newcommand {\EAppFnStep}    {\ruleName{E-App1}}
\newcommand {\EAppArgStep}   {\ruleName{E-App2}}
\newcommand {\EAppBeta}      {\ruleName{E-App-Abs}}
\newcommand {\EAbsStep}      {\ruleName{E-Abs}}

\newcommand {\MRef}          {\ruleName{M-Ref}}
\newcommand {\MTr}           {\ruleName{M-Tr}}
\newcommand {\MStep}         {\ruleName{M-Step}}
\newcommand {\MOne}          {\ruleName{M-One-Step}}

\newcommand {\NVZero}        {\ruleName{Nv-Zero}}
\newcommand {\NVSucc}        {\ruleName{Nv-Succ}}

\newcommand {\VNumValue}     {\ruleName{V-NumValue}}
\newcommand {\VZero}         {\ruleName{V-Zero}}
\newcommand {\VTrue}         {\ruleName{V-True}}
\newcommand {\VFalse}        {\ruleName{V-False}}
\newcommand {\VSucc}         {\ruleName{V-Succ}}                 % to be deleted

\newcommand {\BAnno}         {\ruleName{B-Anno}}
\newcommand {\BAnnoFn}       {\ruleName{B-Anno-Fn}}
\newcommand {\BAnnoNonFn}    {\ruleName{B-Anno-Non-Fn}}
\newcommand {\BIFT}          {\ruleName{B-IfTrue}}
\newcommand {\BIFF}          {\ruleName{B-IfFalse}}
\newcommand {\BOp}           {\ruleName{B-Op}}
\newcommand {\BPlus}         {\ruleName{B-Plus}}
\newcommand {\BEq}           {\ruleName{B-Eq}}
\newcommand {\BLet}          {\ruleName{B-Let}}
\newcommand {\BNum}          {\ruleName{B-Num}}
\newcommand {\BVar}          {\ruleName{B-Var}}
\newcommand {\BIF}           {\ruleName{B-If}}
\newcommand {\BTrue}         {\ruleName{B-True}}
\newcommand {\BFalse}        {\ruleName{B-False}}
\newcommand {\BFun}          {\ruleName{B-Fun}}
\newcommand {\BRec}          {\ruleName{B-Rec}}

\newcommand {\BValue}        {\ruleName{B-Value}}
\newcommand {\BIfTrue}       {\ruleName{B-IfTrue}}
\newcommand {\BIfFalse}      {\ruleName{B-IfFalse}}
\newcommand {\BSucc}         {\ruleName{B-Succ}}
\newcommand {\BPredZero}     {\ruleName{B-PredZero}}
\newcommand {\BPredSucc}     {\ruleName{B-PredSucc}}
\newcommand {\BIszeroZero}   {\ruleName{B-IszeroZero}}
\newcommand {\BIszeroSucc}   {\ruleName{B-IszeroSucc}}

\newcommand {\BLetn}         {\ruleName{B-Letn}}
\newcommand {\BLetp}         {\ruleName{B-LetPair}}
\newcommand {\BPair}         {\ruleName{B-Pair}}
\newcommand {\BFst}          {\ruleName{B-Fst}}
\newcommand {\BSnd}          {\ruleName{B-Snd}}
\newcommand {\BFn}           {\ruleName{B-Fn}}
\newcommand {\BApp}          {\ruleName{B-App}}

\newcommand {\Rsectintro}    {\ruleName{$\sectty$intro}}
\newcommand {\Rsectelim} [1] {\ruleName{$\sectty$elim{#1}}}


%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
