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

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