
% -- Environments -------------------------------------------------------------
\newtheorem{theorem}	{Theorem}	[section]
\newtheorem{lemma}	{Lemma}		[section]
\newtheorem{definition}	{Definition}	[section]


% -- Meta commands ------------------------------------------------------------
\newcommand{\note}	[1]	{\textbf{(NOTE: #1)}}
\newcommand{\TODO}	[1]	{\textbf{(TODO:~ #1)}}

% -- Brackets -----------------------------------------------------------------
\newcommand{\apair}	[1]	{ \langle#1\rangle }
\newcommand{\setof}	[1]	{ \{#1\} }

% -- 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\To			{\Rightarrow}
\newcommand\toa[1]		{\stackrel{#1}{\rightarrow}}
\newcommand\longto		{\longrightarrow}
\newcommand\longtoa[1]		{\stackrel{#1}{\longrightarrow}}
\newcommand\eto			{\longrightarrow}
\newcommand\lto			{\leadsto}
\newcommand\ltoa[1]		{\stackrel{#1}{\leadsto}}
\newcommand\mtoa[1]		{\stackrel{#1}{\mapsto}}
\newcommand\tme			{\sqsupseteq}
\newcommand\tle			{\sqsubseteq}
\newcommand\equalsdef		{\stackrel{\trm{\tiny{def}}}{=}}
\newcommand\equalsobs		{\stackrel{\trm{\tiny{obs}}}{=}}


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

\newcommand{\kiPi}	[3]	{\Pi(#1 : #2). \: #3}


% -- Term Macros --------------------------------------------------------------
\newcommand{\teLAM}	[3]	{\Lambda(#1 : #2). \: #3}
\newcommand{\teLAMB}	[4]	{\Lambda(#1 \sqsupseteq #2 : #3). \: #4}
\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{\teWithR}	[3]	{\kwithregion~ #1 ~\kof~ #2~ \kin \ #3}
\newcommand{\teIf}	[3]	{\kif \ #1 \ \kthen \ #2 \ \kelse \ #3}
\newcommand{\teMask}	[2]	{\kmask~ #1~ \kin~ #2}

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

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

% -- superkind judgement
\newcommand{\ksJudge}	[4]	{#1 \: \arrowvert \: #2 \: \vdash_\textrm{\tiny{K}}#3 \: :: \: #4}
\newcommand{\ksJudgeGS}	[2]	{\ksJudge{\Gamma}{\Sigma}{#1}{#2}}
\newcommand{\ksJudgeES}	[2]	{\ksJudge{\emptyset}{\Sigma}{#1}{#2}}

% -- 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{\suJudgeES}	[2]	{\suJudge{\emptyset}	{\Sigma}{#1}{#2}}

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

% -- witness constructon
\newcommand{\wcJudge}	[3]	{#1 \: ; \: #2 \lto #3}

% -- term evaluation
\newcommand{\evJudge}	[4]	{#1 \: ; \: #2 \longrightarrow #3 \: ; \; #4}
\newcommand{\evJudgeHH}	[2]	{\evJudge{H}{#1}{H}{#2}}

% -- big step evaluation
\newcommand{\eiJudge}	[5]	{#1 \: ; \: #2 \downarrow #3 \: ; \; #4 \; \vdash #5}

% -- big step witness construction
\newcommand{\wiJudge}	[4]	{#1 \: ; \: #2 \:\rotatebox[origin=c]{270}{$\leadsto$}~ #3 \; \vdash #4}

% -- pure effects
\newcommand{\pureJudge}	[2]	{#1 \; \vdash \; #2~~ \trm{\tbf{pure}}}
\newcommand{\pureJudgeS}[1]	{\pureJudge{\Sigma}{#1}}

% -- residues
\newcommand{\Residue}		{\textbf{R}}


% -- Code Blocks --------------------------------------------------------------
\newcommand{\code}[1]{
	\programmath
	\[ 
	\begin{array}{llllllllllllllll}
	#1 
	\end{array}
	\]
	\unprogrammath}

% -- Boxes --------------------------------------------------------------------
\newcommand{\boxfig}[1]{
	\fbox{
	\begin{minipage}{12cm}
	#1
	\end{minipage}
	}
}

% -- 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]{
	#2
	\ \textrm{\ (#1)}
}

% -- A type rule
\newcommand{\ruleI}[2]{\frac{#1}{#2}}

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


% -- Proof Stuff --------------------------------------------------------------



\newcommand{\pProof}		{ \tbf{Proof: } }

\newcommand{\pIf}		{ \trm{If} \ }
\newcommand{\pthen}		{ \ \trm{then} \ }
\newcommand{\pand}		{ \ \trm{and} \ }
\newcommand{\por}		{ \ \ \trm{or} \ \ }
\newcommand{\pstep}	[2]	{ #1 \: ; \: #2 \ \trm{can step}}
\newcommand{\pCase}	[1]	{ \tbf{Case}: \ #1 }
\newcommand{\pcase}	[1]	{ \emph{Case}: \ #1}
\newcommand{\pby}	[1]	{ \textrm{(#1)}	}
\newcommand{\pnofab}	[1]	{ \textrm{nofab}(#1) }

\newcommand{\sims}		{\sim_\Sigma}
\newcommand{\heap}		{\textrm{H}}

\newcommand{\statement} [1] 
{
	\begin{tabular}{ll}
	#1
	\end{tabular}
	\smallskip
}

\newcommand{\tabbedstmts} [1]
{
	\begin{tabbing}
	MMMM 	\= MMMMMMMMMMMMMMMMMMMMMMMMMM \= MMM \kill
	#1
	\end{tabbing}
}
