- matex: minor improvements

[helm.git] / matita / components / binaries / matex / test / basic_1.sty

diff --git a/matita/components/binaries/matex/test/basic_1.sty b/matita/components/binaries/matex/test/basic_1.sty
index dc89b09c06c85fefa414f02e97e6a337453b6623..4cf4066988e8b64ff0cf89d29d13d8075addb0fb 100644 (file)
--- a/matita/components/binaries/matex/test/basic_1.sty
+++ b/matita/components/binaries/matex/test/basic_1.sty
@@ -1,25 +1,74 @@
 \NeedsTeXFormat{LaTeX2e}[1995/12/01]
-\ProvidesPackage{basic_1}[2016/06/19 Notation for "cic:/matita/lambdadelta/basic_1/"]
+\ProvidesPackage{basic_1}[2016/06/21 Notation for "cic:/matita/lambdadelta/basic_1/"]
 \RequirePackage{legacy_1}
 \RequirePackage{ground_1}
 \ExecuteOptions{}
 \ProcessOptions*
 
+\let\OldEquiv=\Equiv
+
 \makeatletter
 
-\newcommand*\ld@drop[1]{\setordlink{\Downarrow}{#1}}
-\newcommand*\ld@drops[1]{\setordlink{\Downarrow^*}{#1}}
-\newcommand*\ld@funlift[1]{\setordlink{\uparrow}{#1}}
-\newcommand*\ld@funlifts[1]{\setordlink{\uparrow^*}{#1}}
+\newcommand*\ld@ob[1]{\mathopen{[}}
+\newcommand*\ld@cb[1]{\mathopen{]}}
+\newcommand*\ld@oB[1]{\mathopen{\lBrack}}
+\newcommand*\ld@cB[1]{\mathopen{\rBrack}}
+
+\newcommand*\ld@coweight[1]{\setoplink{\equivVvert}{#1}{}}
+\newcommand*\ld@drop[2]{\setoplink{\Downarrow}{#1}{#2}}
+\newcommand*\ld@drops[2]{\setoplink{\Downarrow^*}{#1}{#2}}
+\newcommand*\ld@equiv[2]{\setrellink{\equiv}{#1}{#2}}
+\newcommand*\ld@funlift[2]{\setoplink{\uparrow}{#1}{#2}}
+\newcommand*\ld@funlifts[2]{\setoplink{\uparrow^*}{#1}{}}
+\newcommand*\ld@funv[2]{\setoplink{\mathsf{v}}{#1}{#2}}
+\newcommand*\ld@funw[2]{\setoplink{\mathsf{w}}{#1}{#2}}
+\newcommand*\ld@leaf[1]{\setoplink{\star}{#1}{}}
+\newcommand*\ld@length@open[1]{\setopenlink{\vert}{#1}}
+\newcommand*\ld@length@close[1]{\setcloselink{\vert}{#1}}
+\newcommand*\ld@lenv[1]{\setoplink{\mathsf{lenv}}{#1}{}}
+\newcommand*\ld@level[1]{\setoplink{\mathsf{level}}{#1}{}}
+\newcommand*\ld@lref[1]{\setoplink{\#}{#1}{}}
+\newcommand*\ld@next[2]{\setoplink{\mathsf{next}}{#1}{#2}}
+\newcommand*\ld@sametop[1]{\setrellink{\eqsim}{#1}{}}
+\newcommand*\ld@shift[1]{\setordlink{.}{#1}}
+\newcommand*\ld@subst[1]{\setbinlink{/}{#1}{}}
+\newcommand*\ld@substs[1]{\setbinlink{/^*}{#1}{}}
+\newcommand*\ld@to[1]{\setrellink{\rightarrow}{#1}{}}
+\newcommand*\ld@weight[1]{\setoplink{\equalparallel}{#1}{}}
 
 \newcommand*\ld@tuple@a[2]{\ld@oa{#1}#2\ld@ca{#1}}
 
+\newcommand*\AtomA[2]{\ld@leaf{#1}#2}
+\newcommand*\AtomB[3]{\ld@leaf{#1}\ld@tuple@b{#1}{#2}{#3}}
+\newcommand*\CoConsA[3]{#2\ld@cocons{#1}#3}
 \newcommand*\ConsA[3]{#2\ld@cons{#1}#3}
-\newcommand*\Drop[5]{\ld@drop{#1}\ld@tuple@b{#1}{#2}{#3}\ma@thop{}#4\ld@eq{#1}#5}
-\newcommand*\DropS[4]{\ld@drops{#1}\ld@tuple@a{#1}{#2}\ma@thop{}#3\ld@eq{#1}#4}
-\newcommand*\FunLift[4]{\ld@funlift{#1}\ld@tuple@b{#1}{#2}{#3}\ma@thop{}#4}
-\newcommand*\FunLiftS[3]{\ld@funlifts{#1}\ld@tuple@a{#1}{#2}\ma@thop{}#3}
-\newcommand*\RevConsA[3]{#2\ld@revcons{#1}#3}
+\newcommand*\CoWeightA[2]{\ld@coweight{#1}\ld@tuple@a{#1}{#2}}
+\newcommand*\CoWeightB[3]{\ld@coweight{#1}\ld@tuple@b{#1}{#2}{#3}}
+\newcommand*\Drop[3]{\ld@drop{#1}{}#2\ld@eq{#1}#3}
+\newcommand*\DropA[4]{\ld@drop{#1}{\ld@tuple@a{#1}{#2}}#3\ld@eq{#1}#4}
+\newcommand*\DropB[5]{\ld@drop{#1}{\ld@tuple@b{#1}{#2}{#3}}#4\ld@eq{#1}#5}
+\newcommand*\DropS[4]{\ld@drops{#1}{\ld@tuple@a{#1}{#2}}#3\ld@eq{#1}#4}
+\renewcommand*\Equiv[3]{#2\ld@equiv{#1}{}#3}
+\newcommand*\EquivA[4]{#3\ld@equiv{#1}{\ld@tuple@a{#1}{#2}}#4}
+\newcommand*\FunLift[4]{\ld@funlift{#1}{\ld@tuple@b{#1}{#2}{#3}}#4}
+\newcommand*\FunLiftS[3]{\ld@funlifts{#1}{\ld@tuple@a{#1}{#2}}#3}
+\newcommand*\FunSubstS[4]{\mathop{\ld@ob{#1}#3\ld@substs{#1}#2\ld@cb{#1}}#4}
+\newcommand*\FunV[3]{\ld@funv{#1}{\ld@tuple@a{#1}{#2}}#3}
+\newcommand*\FunW[3]{\ld@funw{#1}{\ld@tuple@a{#1}{#2}}#3}
+\newcommand*\LEnv[2]{\ld@lenv{#1}#2}
+\newcommand*\Length[2]{\ld@length@open{#1}#2\ld@length@close{#1}}
+\newcommand*\Level[2]{\ld@level{#1}#2}
+\newcommand*\LRef[2]{\ld@lref{#1}#2}
+\newcommand*\LTB[5]{\ld@tuple@b{#1}{#2}{#3}\ld@lt{#1}\ld@tuple@b{#1}{#4}{#5}}
+\newcommand*\Next[3]{\ld@next{#1}{\ld@tuple@a{#1}{#2}}#3}
+\newcommand*\SameTop[3]{#2\ld@sametop{#1}#3}
+\newcommand*\Shift[3]{#2\ld@shift{#1}#3}
+\newcommand*\Subst[5]{\mathop{\ld@oB{#1}#3\ld@subst{#1}#2\ld@cB{#1}}#4\ld@eq{#1}#5}
+\newcommand*\SubstB[7]{\mathop{\ld@oB{#1}#3\ld@subst{#1}#2\ld@cB{#1}}\ld@tuple@b{#1}{#4}{#5}\ld@eq{#1}\ld@tuple@b{#1}{#6}{#7}}
+\newcommand*\SubstS[5]{\mathop{\ld@oB{#1}#3\ld@substs{#1}#2\ld@cB{#1}}#4\ld@eq{#1}#5}
+\newcommand*\To[3]{#2\ld@to{#1}#3}
+\newcommand*\WeightA[2]{\ld@weight{#1}\ld@tuple@a{#1}{#2}}
+\newcommand*\WeightB[3]{\ld@weight{#1}\ld@tuple@b{#1}{#2}{#3}}
 
 \makeatother