

%-------------------------------------------------------------------------------
% General                                                                       
%-------------------------------------------------------------------------------

\newcommand{\Spb}{\ |\ }
\newcommand{\Set}[1]{\{#1\}}
\newcommand{\Card}[1]{\left|#1\right|}
\def\XXX#1{XXX #1 XXX}


%-------------------------------------------------------------------------------
% LF                                                                            
%-------------------------------------------------------------------------------

% General Form
\newcommand{\PiTyp}[3]{\Pi #1 : #2.\ #3}
\newcommand{\Lam}[2]{\lambda #1.\ #2}
\newcommand{\Type}{\mathtt{type}}
\newcommand{\Kind}{\mathtt{kind}}
\newcommand{\Appl}[2]{#1\ #2}
\newcommand{\Of}[2]{#1\ :\ #2}
\newcommand{\LFArrow}{\to}

% Spine Form
\newcommand{\SpPiTyp}[2]{\Pi #1.#2}
\newcommand{\SpLam}[1]{\lambda #1}
\newcommand{\Root}{\mbox{root}}
\newcommand{\Nil}{\mathtt{nil}}

% Type Checking

%% Eager
\newcommand{\CheckTy}[3][\Gamma]{#1\vdash #2 \Leftarrow #3}
\newcommand{\SynthTy}[3][\Gamma]{#1\vdash #2 \Rightarrow #3}
\newcommand{\Focus}[4][\Gamma]{#1\vdash #2 : #3 > #4}
\newcommand{\Equiv}[2]{#1\equiv #2}

%% Lazy
\newcommand{\LzCheckTy}[6][\Gamma]{#1\vdash #2 \Leftarrow #3 > #4 \times #5 \times #6}
\newcommand{\LzFocus}[6][\Gamma]{#1\vdash #2 : #3 > #4 \times #5 \times #6}
\newcommand{\LzEquiv}[4]{#1\equiv #2 > #3 \times #4}

% Substitutions
\newcommand{\Msub}{[\sigma]}
\newcommand{\Ssub}{[1\cdot(\sigma\Comp\Shift)]}
\newcommand{\Comp}{~\circ~}
\newcommand{\App}{~@~}
\newcommand{\Shift}{\uparrow}
\newcommand{\IdSub}{\mathtt{id}}
%% Admissible substitutions
\newcommand{\AdmSub}[3][\Sigma]{#1\vdash #2:#3}
%% Hereditary substitutions
\newcommand{\HerSub}[2][\sigma]{#2[#1]_h}

% Equivalence
\newcommand{\StepsTo}{\rightsquigarrow}
\newcommand{\NoStep}{\not\rightsquigarrow}

% Weak Head Normal Form
\newcommand{\Weak}{\hookrightarrow}

% Sequents
\newcommand{\SeqArr}{\Longrightarrow}
\newcommand{\Sequent}[4][]{#2\ ;\ #3 \SeqArr_{#1} #4}

% Subformulas
\newcommand{\PSubform}[2][\Psi]{\ensuremath{#1\vdash #2^+}}
\newcommand{\NSubform}[2][\Psi]{\ensuremath{#1\vdash #2^-}}

% Unification
\newcommand{\mgu}{\mathit{mgu}}
\newcommand{\MGU}[4][\Sigma]{#1\vdash #2 = \mgu(#3,#4)}
