]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/binaries/matex/test/basic_1.sty
corrections to use less font packages (TeX was complaining)
[helm.git] / matita / components / binaries / matex / test / basic_1.sty
index 27066107555b62e3e1e9e3278a23ab56d6dde183..dc89b09c06c85fefa414f02e97e6a337453b6623 100644 (file)
@@ -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