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

   1 \makeatletter
   2
   3 \newcommand*\setlabel[1]{\protected@edef\@currentlabel{#1}}
   4
   5 \newtheorem{prop}{Proposition}
   6
   7 \newcommand*\ObjLabel[1]{\label{obj:#1}}
   8 \newcommand*\ObjRef[1]{\ref{obj:#1}}
   9
  10 \newcommand*\Object[3]{\begin{prop}[#1]\hfil\\\setlabel{#1}\ObjLabel{#2}#3\end{prop}}
  11
  12 \newcommand*\@skip[2]{}
  13 \newcommand*\Next[3]{\def\@tmp{#3}\ifx\@tmp\empty #2\let\next=\@skip\else #1{#3}\let\next=\Next\fi\next #1#2}
  14
  15 \newcommand*\@proc[1]{ #1}
  16
  17 \newcommand*\PROP{PROP}
  18 \newcommand*\CROP[1]{CROP}
  19 \newcommand*\TYPE[1]{TYPE}
  20 \newcommand*\LREF[2]{#1}
  21 \newcommand*\GREF[2]{#1}
  22 \newcommand*\ABBR[3]{(D #1 #2 #3) }
  23 \newcommand*\ABST[2]{(I #1 #2) }
  24 \newcommand*\PROD[2]{(P #1 #2) }
  25 \newcommand*\APPL{(A)\Next\@proc\relax}
  26 \newcommand*\CASE[3]{(C #1 #2 #3)\Next\@proc\relax}
  27
  28 \def\@arg#1{, #1}
  29 \def\@stop{.\vskip10pt}
  30
  31 \newcommand*\DECL[3]{\textbf{#1} : #3\vskip10pt}
  32 \newcommand*\PRIM{}
  33 \newcommand*\BODY[1]{is #1\vskip10pt}
  34 \newcommand*\STEP[1]{by #1\Next\@arg\@stop}
  35 \newcommand*\DEST[1]{by cases on #1\Next\@arg\@stop}
  36
  37 \makeatother