\NeedsTeXFormat{LaTeX2e}[1995/12/01]
\ProvidesPackage{matex}[2016/02/03 MaTeX Package]
\RequirePackage{xcolor}
\ExecuteOptions{}
\ProcessOptions*

\makeatletter

\definecolor{ma@black}{HTML}{000000}
\definecolor{ma@blue}{HTML}{00005F}
\definecolor{ma@purple}{HTML}{3F005F}

\newcommand*\ma@fwd{ma@black}
\newcommand*\ma@open{ma@blue}
\newcommand*\ma@exit{ma@blue}
\newcommand*\ma@prim{ma@purple}
\newcommand*\ma@qed{ma@blue}

\newcommand*\setlabel[1]{\protected@edef\@currentlabel{#1}}

\newcommand*\ObjLabel[1]{\label{obj:#1}}
\newcommand*\ObjRef[1]{\ref{obj:#1}}

\newtheorem{prop}{Proposition}
\newenvironment{proof}{\setlength\parindent{0pt}}{}
\newenvironment{ma@step}[1]{\color{#1}}{\\}

\newcommand*\Object[3]{\begin{prop}[#1]\hfil\\\setlabel{#1}\ObjLabel{#2}#3\end{prop}}

\newcommand*\ma@tmp{}
\newcommand*\ma@skip[4]{}
\newcommand*\ma@next[5]{\def\ma@tmp{#5}\ifx\ma@tmp\empty #4\let\ma@tmp=\ma@skip\else #1#2{#5}\let\ma@tmp=\ma@next\fi\ma@tmp #3#2#3#4}

\newcommand*\ma@space{ }
\newcommand*\ma@arg[1]{#1}

\newcommand*\PROP{PROP}
\newcommand*\CROP[1]{CROP}
\newcommand*\TYPE[1]{TYPE}
\newcommand*\LREF[2]{#1}
\newcommand*\GREF[2]{#1}
\newcommand*\ABBR[3]{(D #1 #2 #3) }
\newcommand*\ABST[2]{(I #1 #2) }
\newcommand*\PROD[2]{(P #1 #2) }
\newcommand*\APPL{(A)\ma@next\ma@space\ma@arg\ma@space\relax}
\newcommand*\CASE[3]{(C #1 #2 #3)\ma@next\ma@space\ma@arg\ma@space\relax}

\newcommand*\ma@with{ with }
\newcommand*\ma@comma{, }
\newcommand*\ma@stop{.\end{ma@step}}
\newcommand*\ma@head[4]{\def\ma@tmp{#4}%
   \ifx\ma@tmp\empty\begin{ma@step}{#1}\textbf{#2}%
   \else\begin{ma@step}{#3}\textbf{#4}%
   \fi
}
\newcommand*\ma@tail{\ma@next\ma@with\ma@arg\ma@comma\ma@stop}

\newcommand*\EXIT[1]{\ma@head{}{}{\ma@exit}{end} of block #1\ma@stop}
\newcommand*\OPEN[3]{\ma@head{}{}{\ma@open}{#1} is this block #3\ma@stop}
\newcommand*\PRIM[3]{\ma@head{}{}{\ma@prim}{#1} will have type #3\ma@stop}
\newcommand*\DECL[3]{\ma@head{\ma@qed}{\_QED}{\ma@fwd}{#1} has type #3\\}
\newcommand*\BODY[1]{being #1\ma@stop}
\newcommand*\STEP[1]{by #1\ma@tail}
\newcommand*\DEST[1]{by cases on #1\ma@tail}

\makeatother

\endinput
