X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fmatex%2Ftest%2Fbasic_1.sty;h=dc89b09c06c85fefa414f02e97e6a337453b6623;hb=da42c465b04bbfc470e73b8060155d1aadd184c5;hp=27066107555b62e3e1e9e3278a23ab56d6dde183;hpb=c992745a40b4ac8b6c5285bf9c5eff26c423f236;p=helm.git diff --git a/matita/components/binaries/matex/test/basic_1.sty b/matita/components/binaries/matex/test/basic_1.sty index 270661075..dc89b09c0 100644 --- a/matita/components/binaries/matex/test/basic_1.sty +++ b/matita/components/binaries/matex/test/basic_1.sty @@ -1,10 +1,26 @@ \NeedsTeXFormat{LaTeX2e}[1995/12/01] -\ProvidesPackage{basic_1}[2016/05/23 Notation for "cic:/matita/lambdadelta/basic_1/"] +\ProvidesPackage{basic_1}[2016/06/19 Notation for "cic:/matita/lambdadelta/basic_1/"] +\RequirePackage{legacy_1} +\RequirePackage{ground_1} \ExecuteOptions{} \ProcessOptions* \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@tuple@a[2]{\ld@oa{#1}#2\ld@ca{#1}} + +\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} + \makeatother \endinput