1 \NeedsTeXFormat{LaTeX2e}[1995/12/01]
2 \ProvidesPackage{matex}[2015/12/21 MaTeX Package]
8 \newcommand*\setlabel[1]{\protected@edef\@currentlabel{#1}}
10 \newcommand*\ObjLabel[1]{\label{obj:#1}}
11 \newcommand*\ObjRef[1]{\ref{obj:#1}}
13 \newtheorem{prop}{Proposition}
14 \newenvironment{proof}{\setlength\parindent{0pt}}{}
15 \newenvironment{ma@step}{}{\vskip0pt}
17 \newcommand*\Object[3]{\begin{prop}[#1]\hfil\\\setlabel{#1}\ObjLabel{#2}#3\end{prop}}
20 \newcommand*\ma@skip[4]{}
21 \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}
23 \newcommand*\ma@space{ }
24 \newcommand*\ma@arg[1]{#1}
26 \newcommand*\PROP{PROP}
27 \newcommand*\CROP[1]{CROP}
28 \newcommand*\TYPE[1]{TYPE}
29 \newcommand*\LREF[2]{#1}
30 \newcommand*\GREF[2]{#1}
31 \newcommand*\ABBR[3]{(D #1 #2 #3) }
32 \newcommand*\ABST[2]{(I #1 #2) }
33 \newcommand*\PROD[2]{(P #1 #2) }
34 \newcommand*\APPL{(A)\ma@next\ma@space\ma@arg\ma@space\relax}
35 \newcommand*\CASE[3]{(C #1 #2 #3)\ma@next\ma@space\ma@arg\ma@space\relax}
37 \newcommand*\ma@with{ with }
38 \newcommand*\ma@comma{, }
39 \newcommand*\ma@stop{.\end{ma@step}}
41 \newcommand*\DECL[3]{\def\ma@tmp{#1}\begin{ma@step}\textbf{\ifx\ma@tmp\empty\_conlusion\else #1\fi} of type #3}
42 \newcommand*\PRIM{\end{ma@step}}
43 \newcommand*\BODY[1]{\\is #1\end{ma@step}}
44 \newcommand*\STEP[1]{\\by #1\ma@next\ma@with\ma@arg\ma@comma\ma@stop}
45 \newcommand*\DEST[1]{\\by cases on #1\ma@next\ma@with\ma@arg\ma@comma\ma@stop}
46 \newcommand*\OPEN[3]{\begin{ma@step}\textbf{#1} is the following scope #3.\end{ma@step}}
47 \newcommand*\EXIT[1]{\begin{ma@step}\textbf{end} of scope #1.\end{ma@step}}