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

   1 \NeedsTeXFormat{LaTeX2e}[1995/12/01]
   2 \ProvidesPackage{basic_1}[2016/06/24 Notation for "cic:/matita/lambdadelta/basic_1/"]
   3 \RequirePackage{legacy_1}
   4 \RequirePackage{ground_1}
   5 \ExecuteOptions{}
   6 \ProcessOptions*
   7
   8 \let\OldEquiv=\Equiv
   9
  10 \makeatletter
  11
  12 \newcommand*\ld@ob[1]{\mathopen{[}}
  13 \newcommand*\ld@cb[1]{\mathopen{]}}
  14 \newcommand*\ld@oB[1]{\mathopen{\lBrack}}
  15 \newcommand*\ld@cB[1]{\mathopen{\rBrack}}
  16 \newcommand*\ld@env[1]{\mathrel{\vdash}}
  17
  18 \newcommand*\ld@arity[2]{\setrellink{\mathsf{arity}}{#1}{#2}}
  19 \newcommand*\ld@coconverts[1]{\setrellink{\mathsf{convert}_{\mathord\oplusrhrim}^*}{#1}{}}
  20 \newcommand*\ld@convert[1]{\setrellink{\mathsf{convert}}{#1}{}}
  21 \newcommand*\ld@converts[1]{\setrellink{\mathsf{convert}^*}{#1}{}}
  22 \newcommand*\ld@coweight[1]{\setoplink{\equivVvert}{#1}{}}
  23 \newcommand*\ld@drop[2]{\setoplink{\Downarrow}{#1}{#2}}
  24 \newcommand*\ld@drops[2]{\setoplink{\Downarrow^*}{#1}{#2}}
  25 \newcommand*\ld@equiv[2]{\setrellink{\equiv}{#1}{#2}}
  26 \newcommand*\ld@funlift[2]{\setoplink{\uparrow}{#1}{#2}}
  27 \newcommand*\ld@funlifts[2]{\setoplink{\uparrow^*}{#1}{}}
  28 \newcommand*\ld@funv[2]{\setoplink{\mathsf{v}}{#1}{#2}}
  29 \newcommand*\ld@funw[2]{\setoplink{\mathsf{w}}{#1}{#2}}
  30 \newcommand*\ld@in[1]{\setrellink{\in}{#1}{}}
  31 \newcommand*\ld@leaf[1]{\setoplink{\star}{#1}{}}
  32 \newcommand*\ld@length@open[1]{\setopenlink{\vert}{#1}}
  33 \newcommand*\ld@length@close[1]{\setcloselink{\vert}{#1}}
  34 \newcommand*\ld@lenv[1]{\setoplink{\mathsf{lenv}}{#1}{}}
  35 \newcommand*\ld@level[1]{\setoplink{\mathsf{level}}{#1}{}}
  36 \newcommand*\ld@lref[1]{\setoplink{\#}{#1}{}}
  37 \newcommand*\ld@next[2]{\setoplink{\mathsf{next}}{#1}{#2}}
  38 \newcommand*\ld@rcandidate[2]{\setoplink{\mathsf{r\_candidate}}{#1}{#2}}
  39 \newcommand*\ld@rnormal[1]{\setoplink{\mathsf{r\_normal}}{#1}{}}
  40 \newcommand*\ld@rstep[1]{\setrellink{\mathsf{r\_step}}{#1}{}}
  41 \newcommand*\ld@rsteps[1]{\setrellink{\mathsf{r\_step^*}}{#1}{}}
  42 \newcommand*\ld@rstrong[1]{\setoplink{\mathsf{r\_strong}}{#1}{}}
  43 \newcommand*\ld@sametop[1]{\setrellink{\eqsim}{#1}{}}
  44 \newcommand*\ld@shift[1]{\setordlink{.}{#1}}
  45 \newcommand*\ld@subst[1]{\setbinlink{/}{#1}{}}
  46 \newcommand*\ld@substs[1]{\setbinlink{/^*}{#1}{}}
  47 \newcommand*\ld@to[1]{\setrellink{\rightarrow}{#1}{}}
  48 \newcommand*\ld@tstep[2]{\setrellink{\mathsf{t\_step}}{#1}{#2}}
  49 \newcommand*\ld@tsteps[2]{\setrellink{\mathsf{t\_step^*}}{#1}{#2}}
  50 \newcommand*\ld@type[2]{\setrellink{\mathsf{type}}{#1}{#2}}
  51 \newcommand*\ld@valid[2]{\setoplink{\mathsf{valid}}{#1}{#2}}
  52 \newcommand*\ld@weight[1]{\setoplink{\equalparallel}{#1}{}}
  53
  54 \newcommand*\ld@tuple@a[2]{\ld@oa{#1}#2\ld@ca{#1}}
  55
  56 \newcommand*\Arity[5]{#3\ld@env{#1}#4\ld@arity{#1}{\ld@tuple@a{#1}{#2}}#5}
  57 \newcommand*\AtomA[2]{\ld@leaf{#1}#2}
  58 \newcommand*\AtomB[3]{\ld@leaf{#1}\ld@tuple@b{#1}{#2}{#3}}
  59 \newcommand*\CoConsA[3]{#2\ld@cocons{#1}#3}
  60 \newcommand*\CoConvertS[4]{#2\ld@env{#1}#3\ld@coconverts{#1}#4}
  61 \newcommand*\ConsA[3]{#2\ld@cons{#1}#3}
  62 \newcommand*\Convert[4]{#2\ld@env{#1}#3\ld@convert{#1}#4}
  63 \newcommand*\ConvertS[4]{#2\ld@env{#1}#3\ld@converts{#1}#4}
  64 \newcommand*\CoWeightA[2]{\ld@coweight{#1}\ld@tuple@a{#1}{#2}}
  65 \newcommand*\CoWeightB[3]{\ld@coweight{#1}\ld@tuple@b{#1}{#2}{#3}}
  66 \newcommand*\Drop[3]{\ld@drop{#1}{}#2\ld@eq{#1}#3}
  67 \newcommand*\DropA[4]{\ld@drop{#1}{\ld@tuple@a{#1}{#2}}#3\ld@eq{#1}#4}
  68 \newcommand*\DropB[5]{\ld@drop{#1}{\ld@tuple@b{#1}{#2}{#3}}#4\ld@eq{#1}#5}
  69 \newcommand*\DropS[4]{\ld@drops{#1}{\ld@tuple@a{#1}{#2}}#3\ld@eq{#1}#4}
  70 \renewcommand*\Equiv[3]{#2\ld@equiv{#1}{}#3}
  71 \newcommand*\EquivA[4]{#3\ld@equiv{#1}{\ld@tuple@a{#1}{#2}}#4}
  72 \newcommand*\FunLift[4]{\ld@funlift{#1}{\ld@tuple@b{#1}{#2}{#3}}#4}
  73 \newcommand*\FunLiftS[3]{\ld@funlifts{#1}{\ld@tuple@a{#1}{#2}}#3}
  74 \newcommand*\FunSubstS[4]{\mathop{\ld@ob{#1}#3\ld@substs{#1}#2\ld@cb{#1}}#4}
  75 \newcommand*\FunV[3]{\ld@funv{#1}{\ld@tuple@a{#1}{#2}}#3}
  76 \newcommand*\FunW[3]{\ld@funw{#1}{\ld@tuple@a{#1}{#2}}#3}
  77 \newcommand*\LEnv[2]{\ld@lenv{#1}#2}
  78 \newcommand*\Length[2]{\ld@length@open{#1}#2\ld@length@close{#1}}
  79 \newcommand*\Level[2]{\ld@level{#1}#2}
  80 \newcommand*\LRef[2]{\ld@lref{#1}#2}
  81 \newcommand*\LTB[5]{\ld@tuple@b{#1}{#2}{#3}\ld@lt{#1}\ld@tuple@b{#1}{#4}{#5}}
  82 \newcommand*\Next[3]{\ld@next{#1}{\ld@tuple@a{#1}{#2}}#3}
  83 \newcommand*\RCandidate[5]{\ld@tuple@b{#1}{#3}{#4}\ld@in{#1}\ld@rcandidate{#1}{\ld@tuple@a{#1}{#2}}#5}
  84 \newcommand*\RNormal[3]{#2\ld@env{#1}\ld@rnormal{#1}#3}
  85 \newcommand*\RStep[3]{#2\ld@rstep{#1}#3}
  86 \newcommand*\RStepA[4]{#2\ld@env{#1}#3\ld@rstep{#1}#4}
  87 \newcommand*\RStepS[3]{#2\ld@rsteps{#1}#3}
  88 \newcommand*\RStepSA[4]{#2\ld@env{#1}#3\ld@rsteps{#1}#4}
  89 \newcommand*\RStrong[3]{#2\ld@env{#1}\ld@rstrong{#1}#3}
  90 \newcommand*\SameTop[3]{#2\ld@sametop{#1}#3}
  91 \newcommand*\Shift[3]{#2\ld@shift{#1}#3}
  92 \newcommand*\Subst[5]{\mathop{\ld@oB{#1}#3\ld@subst{#1}#2\ld@cB{#1}}#4\ld@eq{#1}#5}
  93 \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}}
  94 \newcommand*\SubstS[5]{\mathop{\ld@oB{#1}#3\ld@substs{#1}#2\ld@cB{#1}}#4\ld@eq{#1}#5}
  95 \newcommand*\To[3]{#2\ld@to{#1}#3}
  96 \newcommand*\TStep[5]{#3\ld@env{#1}#4\ld@tstep{#1}{\ld@tuple@a{#1}{#2}}#5}
  97 \newcommand*\TStepS[5]{#3\ld@env{#1}#4\ld@tsteps{#1}{\ld@tuple@a{#1}{#2}}#5}
  98 \newcommand*\Type[5]{#3\ld@env{#1}#4\ld@type{#1}{\ld@tuple@a{#1}{#2}}#5}
  99 \newcommand*\Valid[4]{\ld@valid{#1}{\ld@tuple@a{#1}{#2}}#3\ld@eq{#1}#4}
 100 \newcommand*\WeightA[2]{\ld@weight{#1}\ld@tuple@a{#1}{#2}}
 101 \newcommand*\WeightB[3]{\ld@weight{#1}\ld@tuple@b{#1}{#2}{#3}}
 102
 103 \makeatother
 104
 105 \endinput