X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fmatex%2Ftest%2Fmatex.sty;h=b01223fefec60774fc182dabebde22033d01edea;hb=28e8954fbe2e28f01ae918c8d0e0ef34bd84b48f;hp=195789fe3a64c888e34c2b9d020dd97a471840b2;hpb=21679cd1397d9c51519dbe439c29c1683b91ec64;p=helm.git diff --git a/matita/components/binaries/matex/test/matex.sty b/matita/components/binaries/matex/test/matex.sty index 195789fe3..b01223fef 100644 --- a/matita/components/binaries/matex/test/matex.sty +++ b/matita/components/binaries/matex/test/matex.sty @@ -1,16 +1,128 @@ -\newcommand*\Skip[1]{} -\newcommand*\Next[2]{\def\TMP{#2}\ifx\TMP\empty\let\next=\Skip\else #1{#2}\let\next=\Next\fi\next #1} - -\newcommand*\Visit[1]{ #1} - -\newcommand*\Prop{PROP} -\newcommand*\Crop[1]{CROP} -\newcommand*\Type[1]{TYPE} -\newcommand*\LRef[1]{(L #1)} -\newcommand*\GRef[2]{(G #2)\Next\Skip} -\newcommand*\IRef[1]{(J #1)\Next\Skip} -\newcommand*\Abbr[3]{(D #1 #2 #3) } -\newcommand*\Abst[2]{(I #1 #2) } -\newcommand*\Prod[2]{(P #1 #2) } -\newcommand*\Appl{(A)\Next\Visit} -\newcommand*\Case[3]{(C #1 #2 #3)\Next\Visit} +\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