matita/components/binaries/matex/test/matex.sty

   1 \NeedsTeXFormat{LaTeX2e}[1995/12/01]
   2 \ProvidesPackage{matex}[2016/05/22 MaTeX Package]
   3 \RequirePackage{xcolor}
   4 \ExecuteOptions{}
   5 \ProcessOptions*
   6
   7 \makeatletter
   8
   9 \definecolor{ma@black}{HTML}{000000}
  10 \definecolor{ma@blue}{HTML}{00005F}
  11 \definecolor{ma@purple}{HTML}{3F005F}
  12
  13 \newcommand*\ma@fwd{ma@black}
  14 \newcommand*\ma@open{ma@blue}
  15 \newcommand*\ma@exit{ma@blue}
  16 \newcommand*\ma@prim{ma@purple}
  17 \newcommand*\ma@qed{ma@blue}
  18
  19 \newcommand*\neverindent{\setlength\parindent{0pt}}
  20
  21 %\newcommand*\setlabel[1]{\protected@edef\@currentlabel{#1}}
  22 %\newcommand*\ObjLabel[1]{\label{obj:#1}\hypertarget{obj:#1}{}}
  23 %\newcommand*\ObjRef[1]{\hyperlink{obj:#1}{\ref*{obj:#1}}}
  24 %\newcommand*\ma@setlabel[2]{\setlabel{#1}\ObjLabel{#2}}
  25
  26 \newcommand*\ma@settarget[2]{\hypertarget{obj:#2}{#1}}
  27 \newcommand*\ma@setlink[2]{\hyperlink{obj:#2}{#1}}
  28
  29 \newcommand*\ObjIncNode{}
  30 \newcommand*\ObjNode{}
  31
  32 \newcommand*\ma@thehead[3]{\ObjIncNode\textbf{#1 \ObjNode(\ma@settarget{#2}{#3})}\neverindent\par}
  33 \newcommand*\ma@theneck[1]{\textsl{#1}\neverindent\par}
  34
  35 \newenvironment{axiom}[2]{\ma@thehead{Axiom}{#1}{#2}}{\par}
  36 \newenvironment{declaration}[2]{\ma@thehead{Declaration}{#1}{#2}}{\par}
  37 \newenvironment{definition}[2]{}{\par}
  38 \newenvironment{proposition}[2]{\ma@thehead{Proposition}{#1}{#2}}{\par}
  39 \newenvironment{proof}[2]{\ma@theneck{Proof}}{\par}
  40 \newenvironment{ma@step}[1]{\color{#1}}{\par}
  41
  42 \newcommand*\ma@tmp{}
  43 \newcommand*\ma@skip[4]{}
  44 \newcommand*\ma@next[5]{\def\ma@tmp{#5}%
  45    \ifx\ma@tmp\empty #4\let\ma@tmp=\ma@skip\else #1#2{#5}\let\ma@tmp=\ma@next\fi
  46    \ma@tmp #3#2#3#4%
  47 }
  48
  49 \newcommand*\ma@space{ }
  50 \newcommand*\ma@arg[1]{#1}
  51
  52 \newcommand*\ma@setopttarget[2]{\def\ma@tmp{#2}%
  53    \ifx\ma@tmp\empty #1\else\ma@settarget{#1}{#2}\fi
  54 }
  55
  56 \newcommand*\PROP{PROP}
  57 \newcommand*\CROP[1]{CROP}
  58 \newcommand*\TYPE[1]{TYPE}
  59 \newcommand*\LREF[2]{\def\ma@tmp{#2}%
  60    \ifx\ma@tmp\empty #1\else\ma@setlink{#1}{#2}\fi
  61 }
  62 \newcommand*\GREF[2]{\ma@setlink{#1}{#2}}
  63 \newcommand*\ABBR[4]{(D \ma@setopttarget{#1}{#2} #3 #4) }
  64 \newcommand*\ABST[3]{(I \ma@setopttarget{#1}{#2} #3) }
  65 \newcommand*\PROD[3]{(P \ma@setopttarget{#1}{#2} #3) }
  66 \newcommand*\APPL{(A)\ma@next\ma@space\ma@arg\ma@space\relax}
  67 \newcommand*\CASE[3]{(C #1 #2 #3)\ma@next\ma@space\ma@arg\ma@space\relax}
  68
  69 \newcommand*\ma@with{ with }
  70 \newcommand*\ma@comma{, }
  71 \newcommand*\ma@stop{.\end{ma@step}}
  72 \newcommand*\ma@head[6]{\def\ma@tmp{#5}%
  73    \ifx\ma@tmp\empty\begin{ma@step}{#1}\textbf{\ma@setopttarget{#2}{#3}}%
  74    \else\begin{ma@step}{#4}\textbf{\ma@setopttarget{#5}{#6}}%
  75    \fi
  76 }
  77 \newcommand*\ma@tail{\ma@next\ma@with\ma@arg\ma@comma\ma@stop}
  78
  79 \newcommand*\EXIT[1]{\ma@head{}{}{}{\ma@exit}{end}{} of block #1\ma@stop}
  80 \newcommand*\OPEN[3]{\ma@head{}{}{}{\ma@open}{#1}{#2} is this block #3\ma@stop}
  81 \newcommand*\PRIM[3]{\ma@head{}{}{}{\ma@prim}{#1}{#2} will have type #3\ma@stop}
  82 \newcommand*\DECL[3]{\ma@head{\ma@qed}{\_QED}{}{\ma@fwd}{#1}{#2} has type #3\par}
  83 \newcommand*\BODY[1]{being #1\ma@stop}
  84 \newcommand*\STEP[1]{by #1\ma@tail}
  85 \newcommand*\DEST[1]{by cases on #1\ma@tail}
  86
  87 \makeatother
  88
  89 \endinput