\NeedsTeXFormat{LaTeX2e}[1995/12/01]
\ProvidesPackage{matex}[2016/06/21 MaTeX Package]
\RequirePackage{xcolor}
\RequirePackage[lcgreekalpha]{stix}
\ExecuteOptions{}
\ProcessOptions*

\makeatletter

\newcommand*\ma@cast{\mathbin:}
\newcommand*\ma@abbr{\mathrel\eqdef}
\newcommand*\ma@prod{\mathord\Pi}
\newcommand*\ma@arrw{\mathrel\Rightarrow}
\newcommand*\ma@fall{\mathord\forall}
\newcommand*\ma@impl{\mathrel\supset}
\newcommand*\ma@case{\mathrel\questeq}
\newcommand*\ma@caze{\mathrel\mapsto}
\newcommand*\ma@pair{\mathbin\mapsto}

\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*\neverindent{\setlength\parindent{0pt}}

%\newcommand*\setlabel[1]{\protected@edef\@currentlabel{#1}}
%\newcommand*\ObjLabel[1]{\label{obj:#1}\hypertarget{obj:#1}{}}
%\newcommand*\ObjRef[1]{\hyperlink{obj:#1}{\ref*{obj:#1}}}
%\newcommand*\ma@setlabel[2]{\setlabel{#1}\ObjLabel{#2}}

\newcommand*\ma@settarget[2]{\hypertarget{obj:#2}{#1}}
\newcommand*\ma@setlink[2]{\hyperlink{obj:#2}{#1}}
\newcommand*\ma@setopttarget[2]{\def\ma@tmp{#2}%
   \mathord{\ifx\ma@tmp\empty #1\else\ma@settarget{#1}{#2}\fi}%
}
\newcommand*\ma@setoptlink[2]{\def\ma@tmp{#2}%
   \mathord{\ifx\ma@tmp\empty #1\else\ma@setlink{#1}{#2}\fi}%
}

\newcommand*\setordlink[2]{\mathord{\ma@setlink{#1}{#2}}}
\newcommand*\setopenlink[2]{\mathopen{\ma@setlink{#1}{#2}}}
\newcommand*\setcloselink[2]{\mathclose{\ma@setlink{#1}{#2}}}
\newcommand*\setpunctlink[2]{\mathpunct{\ma@setlink{#1}{#2}}}
\newcommand*\setoplink[3]{\mathop{\ma@setlink{#1}{#2}#3}}
\newcommand*\setbinlink[3]{\mathbin{\ma@setlink{#1}{#2}#3}}
\newcommand*\setrellink[3]{\mathrel{\ma@setlink{#1}{#2}#3}}

\newcommand*\ObjIncNode{}
\newcommand*\ObjNode{}

\newcommand*\ma@thehead[3]{\ObjIncNode\textbf{#1 \ObjNode(\ma@settarget{#2}{#3})}\neverindent\par}
\newcommand*\ma@theneck[1]{\textsl{#1}\neverindent\par}

\newenvironment{axiom}[2]{\ma@thehead{Axiom}{#1}{#2}$}{$\par}
\newenvironment{declaration}[2]{\ma@thehead{Declaration}{#1}{#2}$}{$\par}
\newenvironment{definition}[2]{$}{$\par}
\newenvironment{proposition}[2]{\ma@thehead{Proposition}{#1}{#2}$}{$\par}
\newenvironment{proof}[2]{\ma@theneck{Proof}}{\par}
\newenvironment{ma@step}[1]{\color{#1}}{\par}

\newcommand*\ma@tmp{}
\newcommand*\ma@last[4]{#4}
\newcommand*\ma@list[5]{\def\ma@tmp{#5}%
   \ifx\ma@tmp\empty\let\ma@tmp=\ma@last\else #1#2{#5}\let\ma@tmp=\ma@list\fi
   \ma@tmp{#3}{#2}{#3}{#4}%
}
\newcommand*\ma@thop[1]{\mathpunct{#1}\allowbreak}
\newcommand*\ma@cm{\ma@thop{,}}
\newcommand*\ma@or{\mathbin\vert}
\newcommand*\ma@cp{)\allowbreak}
\newcommand*\ma@qm{\mathord{?}}
\newcommand*\ma@arg[1]{#1}
\newcommand*\ma@args{(\ma@list\relax\ma@arg\ma@cm\ma@cp}
\newcommand*\ma@cases{\ma@list\relax\ma@arg\ma@or\relax}
\newcommand*\ma@bind{\ma@thop{}}
\newcommand*\ma@skip[1]{}

\newcommand*\PROP{\mathord\mathrm{PROP}}
\newcommand*\CROP[1]{\mathord\mathrm{CROP}}
\newcommand*\TYPE[1]{\mathord\mathrm{TYPE}}
\newcommand*\LREF[2]{\ma@setoptlink{#1}{#2}}
\newcommand*\GREF[2]{\ma@setoptlink{\mathrm{#1}}{#2}}
\newcommand*\ABBR[4]{(\ma@setopttarget{#1}{#2}\ma@abbr #4\ma@cast #3)\ma@bind}
\newcommand*\ABST[3]{(\ma@setopttarget{#1}{#2}\ma@cast #3)\ma@bind}
\newcommand*\PROD[3]{\def\ma@tmp{#2}%
   \ifx\ma@tmp\empty #3\ma@arrw\else
   (\ma@prod\ma@setopttarget{#1}{#2}\ma@cast #3)\ma@bind\fi
}
\newcommand*\FALL[3]{\def\ma@tmp{#2}%
   \ifx\ma@tmp\empty #3\ma@impl\else
   (\ma@fall\ma@setopttarget{#1}{#2}\ma@cast #3)\ma@bind\fi
}
\newcommand*\APPL[1]{#1\ma@args}
\newcommand*\CASE[3]{#3\ma@case\ma@cases}
\newcommand*\CAZE[3]{#3\ma@caze(\ma@qm\ma@cast #2)\ma@cases}
\newcommand*\PAIR[2]{#1\ma@pair #2}

\newcommand*\ma@term[1]{$#1$}
\newcommand*\ma@with{ with }
\newcommand*\ma@comma{, }
\newcommand*\ma@stop{.\end{ma@step}}
\newcommand*\ma@head[6]{\def\ma@tmp{#5}%
   \ifx\ma@tmp\empty\begin{ma@step}{#1}$\mathbf{\ma@setopttarget{#2}{#3}}$%
   \else\begin{ma@step}{#4}$\mathbf{\ma@setopttarget{#5}{#6}}$%
   \fi
}
\newcommand*\ma@tail{\ma@list\ma@with\ma@term\ma@comma\ma@stop}
\newcommand*\ma@type[1]{\def\ma@tmp{#1}%
   \ifx\ma@tmp\empty\mathrm{(omitted)}\else #1\fi
}

\newcommand*\EXIT[1]{\ma@head{\ma@exit}{end}{}{}{}{} of block #1\ma@stop}
\newcommand*\OPEN[3]{\ma@head{}{}{}{\ma@open}{#1}{#2} is this block #3\ma@stop}
\newcommand*\PRIM[3]{\ma@head{}{}{}{\ma@prim}{#1}{#2} will have type $\ma@type{#3}$\ma@stop}
\newcommand*\DECL[3]{\ma@head{\ma@qed}{\_QED}{}{\ma@fwd}{#1}{#2} has type $\ma@type{#3}$\par}
\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
