

% -- Short forms --------------------------------------------------------------
\newcommand{\trm}	[1]	{\textrm{#1}}
\newcommand{\tbf}	[1]	{\textbf{#1}}
\newcommand{\trb}	[1]	{\textrm{\textbf{#1}}}
\newcommand{\un}	[1]	{\underline{#1}}
\newcommand{\ov}	[1]	{\overline{#1}}
\newcommand{\qq}		{\quad \quad}
\newcommand{\mc}	[2]	{\multicolumn{#1}{l}{#2}}

% -- Operators ----------------------------------------------------------------
\newcommand\equalsdef		{\stackrel{\trm{def}}{=}}
\newcommand\To			{\Rightarrow}
\newcommand\toa[1]		{\stackrel{#1}{\rightarrow}}
\newcommand\longtoa[1]		{\stackrel{#1}{\longrightarrow}}
\newcommand\eto			{\longrightarrow}
\newcommand\lto			{\leadsto}
\newcommand\mtoa[1]		{\stackrel{#1}{\mapsto}}

% -- Type Macros --------------------------------------------------------------
\newcommand{\tyForall}	[3]	{\forall(#1 : #2). \: #3}
\newcommand{\tyForallB}	[3]	{\forall(#1 \sqsupseteq #2). \: #3}


% -- Term Macros --------------------------------------------------------------
\newcommand{\teLAM}	[3]	{\Lambda(#1 : #2). \: #3}
\newcommand{\teLAMB}	[3]	{\Lambda(#1 \sqsupseteq #2). \: #3}
\newcommand{\teLam}	[3]	{\lambda(#1 : #2). \: #3}
\newcommand{\teLet}	[3]	{\klet \ #1 = #2 \ \kin \ #3}
\newcommand{\teLetR}	[3]	{\kletregion \ #1 \ \kwith \ \{ #2 \} \ \kin \ #3}
\newcommand{\teLetRE}	[2]	{\kletregion \ #1 \ \kin \ #2}
\newcommand{\teIf}	[3]	{\kif \ #1 \ \kthen \ #2 \ \kelse \ #3}


% -- Judgements ---------------------------------------------------------------
\newcommand\judge		{\hspace{2pt} \boldsymbol{\vdash} \hspace{2pt}}
\newcommand\judgea[1]		{ \hspace{2pt} \boldsymbol{\vdash_{\textrm{\tiny{#1}}}}}

\newcommand{\judgek}[0]		{\judgea{K}}
\newcommand{\judget}[0]		{\judgea{T}}


% -- superkind judgement
\newcommand{\ksJudge}	[3]	{#1 \: \vdash_\textrm{\tiny{K}}#2 \: :: \: #3}

% -- kind judgement
%	ENV :- TYPE :: KIND
\newcommand{\kiJudge}	[4]	{#1 \: \arrowvert \: #2 \: \vdash_\textrm{\tiny{T}}#3 \: :: \: #4}
\newcommand{\kiJudgeGS}	[2]	{\kiJudge{\Gamma}   {\Sigma}{#1}{#2}}
\newcommand{\kiJudgeES}	[2]	{\kiJudge{\emptyset}{\Sigma}{#1}{#2}}
\newcommand{\kiJudgeS}	[2]	{\boldsymbol{\vdash}_\textrm{\tiny{T}}#1 \: :: \: #2 }

% -- type judgement
%	ENV ; ST :- TERM :: TYPE ; EFFECT
\newcommand{\tyJudge}	[5]	{#1 \: \arrowvert \: #2 \: \vdash \: #3 \: :: \: #4 \: ; \: #5 }
\newcommand{\tyJudgeGS}	[3]	{\tyJudge{\Gamma}   {\Sigma}{#1}{#2}{#3}}
\newcommand{\tyJudgeES} [3]	{\tyJudge{\emptyset}{\Sigma}{#1}{#2}{#3}}


% -- subsumption judgement
\newcommand{\suJudge}	[4]	{#1 \: \arrowvert \: #2 \: \vdash \: #3 \: \sqsubseteq \: #4} 
\newcommand{\suJudgeGS}	[2]	{\suJudge{\Gamma}{\Sigma}{#1}{#2}}

\newcommand{\subs}		{\tle_\Sigma}

% -- Type Rules ---------------------------------------------------------------
\newcommand{\ruleBox}[1]{
	\hspace{-1.5cm}
	\begin{minipage}{1.25\textwidth}
	#1
	\end{minipage}
}

\newcommand{\ruleSkip}{ \\[2.5ex] }

% -- A type axiom with tag
\newcommand{\ruleA}[2]{
	\begin{aligned}
	#2
	\end{aligned}
	\tag{#1}
}

% -- A type axiom with a local tag
\newcommand{\ruleAL}[2]{
	\begin{aligned}
	#2
	\end{aligned}
	\trm{\ (#1)}
}

% -- A type rule with a tag
\newcommand{\ruleI}[3]{
	\frac	{ \begin{aligned}
		  #2
		  \end{aligned}
		}
		{ \begin{aligned}
		  #3
		  \end{aligned}
		}
		\tag{#1}
}

% -- A type rule with a local tag
\newcommand{\ruleIL}[3]{
	\frac	{ \begin{aligned}
		  #2
		  \end{aligned}
		}
		{ \begin{aligned}
		  #3
		  \end{aligned}
		}
		\trm{\ (#1)}
}
