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

   1 \NeedsTeXFormat{LaTeX2e}[1995/12/01]
   2 \ProvidesPackage{matex}[2016/06/05 MaTeX Package]
   3 \RequirePackage{xcolor}
   4 \RequirePackage{stix}
   5 \ExecuteOptions{}
   6 \ProcessOptions*
   7
   8 \makeatletter
   9
  10 \newcommand*\ma@cast{\mathbin:}
  11 \newcommand*\ma@abbr{\mathrel\eqdef}
  12 \newcommand*\ma@prod{\mathord\Pi}
  13 \newcommand*\ma@arrw{\mathrel\Rightarrow}
  14 \newcommand*\ma@fall{\mathord\forall}
  15 \newcommand*\ma@impl{\mathrel\supset}
  16 \newcommand*\ma@case{\mathrel\questeq}
  17
  18 \definecolor{ma@black}{HTML}{000000}
  19 \definecolor{ma@blue}{HTML}{00005F}
  20 \definecolor{ma@purple}{HTML}{3F005F}
  21
  22 \newcommand*\ma@fwd{ma@black}
  23 \newcommand*\ma@open{ma@blue}
  24 \newcommand*\ma@exit{ma@blue}
  25 \newcommand*\ma@prim{ma@purple}
  26 \newcommand*\ma@qed{ma@blue}
  27
  28 \newcommand*\neverindent{\setlength\parindent{0pt}}
  29
  30 %\newcommand*\setlabel[1]{\protected@edef\@currentlabel{#1}}
  31 %\newcommand*\ObjLabel[1]{\label{obj:#1}\hypertarget{obj:#1}{}}
  32 %\newcommand*\ObjRef[1]{\hyperlink{obj:#1}{\ref*{obj:#1}}}
  33 %\newcommand*\ma@setlabel[2]{\setlabel{#1}\ObjLabel{#2}}
  34
  35 \newcommand*\ma@settarget[2]{\hypertarget{obj:#2}{#1}}
  36 \newcommand*\ma@setlink[2]{\hyperlink{obj:#2}{#1}}
  37 \newcommand*\ma@setopttarget[2]{\def\ma@tmp{#2}%
  38    \mathord{\ifx\ma@tmp\empty #1\else\ma@settarget{#1}{#2}\fi}%
  39 }
  40 \newcommand*\ma@setoptlink[2]{\def\ma@tmp{#2}%
  41    \mathord{\ifx\ma@tmp\empty #1\else\ma@setlink{#1}{#2}\fi}%
  42 }
  43
  44 \newcommand*\setordlink[2]{\mathord{\ma@setlink{#1}{#2}}}
  45 \newcommand*\setoplink[2]{\mathop{\ma@setlink{#1}{#2}}}
  46 \newcommand*\setbinlink[2]{\mathbin{\ma@setlink{#1}{#2}}}
  47 \newcommand*\setrellink[2]{\mathrel{\ma@setlink{#1}{#2}}}
  48
  49 \newcommand*\ObjIncNode{}
  50 \newcommand*\ObjNode{}
  51
  52 \newcommand*\ma@thehead[3]{\ObjIncNode\textbf{#1 \ObjNode(\ma@settarget{#2}{#3})}\neverindent\par}
  53 \newcommand*\ma@theneck[1]{\textsl{#1}\neverindent\par}
  54
  55 \newenvironment{axiom}[2]{\ma@thehead{Axiom}{#1}{#2}$}{$\par}
  56 \newenvironment{declaration}[2]{\ma@thehead{Declaration}{#1}{#2}$}{$\par}
  57 \newenvironment{definition}[2]{$}{$\par}
  58 \newenvironment{proposition}[2]{\ma@thehead{Proposition}{#1}{#2}$}{$\par}
  59 \newenvironment{proof}[2]{\ma@theneck{Proof}}{\par}
  60 \newenvironment{ma@step}[1]{\color{#1}}{\par}
  61
  62 \newcommand*\ma@tmp{}
  63 \newcommand*\ma@skip[4]{}
  64 \newcommand*\ma@next[5]{\def\ma@tmp{#5}%
  65    \ifx\ma@tmp\empty #4\let\ma@tmp=\ma@skip\else #1#2{#5}\let\ma@tmp=\ma@next\fi
  66    \ma@tmp #3#2#3#4%
  67 }
  68 \newcommand*\ma@thop[1]{\mathop{#1}\allowbreak}
  69 \newcommand*\ma@cm{\ma@thop{,}}
  70 \newcommand*\ma@or{\mathbin\vert}
  71 \newcommand*\ma@cp{)\allowbreak}
  72 \newcommand*\ma@arg[1]{#1}
  73 \newcommand*\ma@args{(\ma@next\relax\ma@arg\ma@cm\ma@cp}
  74 \newcommand*\ma@cases{\ma@next\relax\ma@arg\ma@or\relax}
  75 \newcommand*\ma@bind{\ma@thop{}}
  76
  77 \newcommand*\PROP{\mathord\mathrm{PROP}}
  78 \newcommand*\CROP[1]{\mathord\mathrm{CROP}}
  79 \newcommand*\TYPE[1]{\mathord\mathrm{TYPE}}
  80 \newcommand*\LREF[2]{\ma@setoptlink{#1}{#2}}
  81 \newcommand*\GREF[2]{\ma@setoptlink{\mathrm{#1}}{#2}}
  82 \newcommand*\ABBR[4]{(\ma@setopttarget{#1}{#2}\ma@abbr #4\ma@cast #3)\ma@bind}
  83 \newcommand*\ABST[3]{(\ma@setopttarget{#1}{#2}\ma@cast #3)\ma@bind}
  84 \newcommand*\PROD[3]{\def\ma@tmp{#2}%
  85    \ifx\ma@tmp\empty #3\ma@arrw\else
  86    (\ma@prod\ma@setopttarget{#1}{#2}\ma@cast #3)\ma@bind\fi
  87 }
  88 \newcommand*\FALL[3]{\def\ma@tmp{#2}%
  89    \ifx\ma@tmp\empty #3\ma@impl\else
  90    (\ma@fall\ma@setopttarget{#1}{#2}\ma@cast #3)\ma@bind\fi
  91 }
  92 \newcommand*\APPL[1]{#1\ma@args}
  93 \newcommand*\CASE[3]{(#3\ma@cast #1)\ma@case\ma@cases}
  94 \newcommand*\NONE{\mathrm{(omitted)}}
  95
  96 \newcommand*\ma@term[1]{$#1$}
  97 \newcommand*\ma@with{ with }
  98 \newcommand*\ma@comma{, }
  99 \newcommand*\ma@stop{.\end{ma@step}}
 100 \newcommand*\ma@head[6]{\def\ma@tmp{#5}%
 101    \ifx\ma@tmp\empty\begin{ma@step}{#1}$\mathbf{\ma@setopttarget{#2}{#3}}$%
 102    \else\begin{ma@step}{#4}$\mathbf{\ma@setopttarget{#5}{#6}}$%
 103    \fi
 104 }
 105 \newcommand*\ma@tail{\ma@next\ma@with\ma@term\ma@comma\ma@stop}
 106
 107 \newcommand*\EXIT[1]{\ma@head{\ma@exit}{end}{}{}{}{} of block #1\ma@stop}
 108 \newcommand*\OPEN[3]{\ma@head{}{}{}{\ma@open}{#1}{#2} is this block #3\ma@stop}
 109 \newcommand*\PRIM[3]{\ma@head{}{}{}{\ma@prim}{#1}{#2} will have type $#3$\ma@stop}
 110 \newcommand*\DECL[3]{\ma@head{\ma@qed}{\_QED}{}{\ma@fwd}{#1}{#2} has type $#3$\par}
 111 \newcommand*\BODY[1]{being $#1$\ma@stop}
 112 \newcommand*\STEP[1]{by $#1$\ma@tail}
 113 \newcommand*\DEST[1]{by cases on $#1$\ma@tail}
 114
 115 \makeatother
 116
 117 \endinput