From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 24 Jun 2016 13:41:09 +0000 (+0000)
Subject: more notation for basic_1 ...
X-Git-Tag: make_still_working~559
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=27e233449243eb4dc9b221a1117607493522c7e9;p=helm.git

more notation for basic_1 ...
---

diff --git a/matita/components/binaries/matex/test/basic_1.conf.xml b/matita/components/binaries/matex/test/basic_1.conf.xml
index 162425ddd..451e77ba5 100644
--- a/matita/components/binaries/matex/test/basic_1.conf.xml
+++ b/matita/components/binaries/matex/test/basic_1.conf.xml
@@ -180,7 +180,9 @@ $(devel.basic1).aplus.defs.aplus.aplus.type 0</key>
     <key name="const">$(devel.basic1).app.defs.cbk.cbk.type Level 1 0</key>
 <!--
 $(devel.basic1).aprem.defs.aprem.aprem.type 0</key>
-$(devel.basic1).arity.defs.arity.arity.type 0</key>
+-->
+    <key name="const">$(devel.basic1).arity.defs.arity.arity.type Arity 4 0</key>
+<!--
 $(devel.basic1).asucc.defs.asucc.asucc.type 0</key>
 $(devel.basic1).C.defs.C.CHead.type 0</key>
 -->
@@ -236,27 +238,23 @@ $(devel.basic1).lift1.defs.trans.trans.type 0</key>
     <key name="const">$(devel.basic1).llt.defs.lweight.lweight.type WeightA 1 0</key>
 <!--
 $(devel.basic1).next_plus.defs.next_plus.next_plus.type 0</key>
-$(devel.basic1).nf2.defs.nf2.type 0</key>
-$(devel.basic1).nf2.defs.nfs2.nfs2.type 0</key>
-$(devel.basic1).pc1.defs.pc1.type 0</key>
-$(devel.basic1).pc3.defs.pc3_left.pc3_left.type 0</key>
-$(devel.basic1).pc3.defs.pc3.type 0</key>
-$(devel.basic1).pr0.defs.pr0.pr0.type 0</key>
-$(devel.basic1).pr1.defs.pr1.pr1.type 0</key>
-$(devel.basic1).pr2.defs.pr2.pr2.type 0</key>
-$(devel.basic1).pr3.defs.pr3.pr3.type 0</key>
 -->
+    <key name="const">$(devel.basic1).nf2.defs.nf2.type RNormal 2 0</key>
+    <key name="const">$(devel.basic1).nf2.defs.nfs2.nfs2.type RNormal 2 0</key>
+    <key name="const">$(devel.basic1).pc1.defs.pc1.type Convert 3 0</key>
+    <key name="const">$(devel.basic1).pc3.defs.pc3_left.pc3_left.type CoConvertS 3 0</key>
+    <key name="const">$(devel.basic1).pc3.defs.pc3.type ConvertS 3 0</key>
+    <key name="const">$(devel.basic1).pr0.defs.pr0.pr0.type RStep 2 0</key>
+    <key name="const">$(devel.basic1).pr1.defs.pr1.pr1.type RStepS 2 0</key>
+    <key name="const">$(devel.basic1).pr2.defs.pr2.pr2.type RStepA 3 0</key>
+    <key name="const">$(devel.basic1).pr3.defs.pr3.pr3.type RStepSA 3 0</key>
     <key name="const">$(devel.basic1).r.defs.r.type FunW 2 0</key>
-<!--
-$(devel.basic1).sc3.defs.sc3.sc3.type 0</key>
--->
+    <key name="const">$(devel.basic1).sc3.defs.sc3.sc3.type RCandidate 4 0</key>
     <key name="const">$(devel.basic1).s.defs.s.type FunV 2 0</key>
-<!--
-$(devel.basic1).sn3.defs.sn3.sn3.type 0</key>
-$(devel.basic1).sn3.defs.sns3.sns3.type 0</key>
-$(devel.basic1).sty0.defs.sty0.sty0.type 0</key>
-$(devel.basic1).sty1.defs.sty1.sty1.type 0</key>
--->
+    <key name="const">$(devel.basic1).sn3.defs.sn3.sn3.type RStrong 2 0</key>
+    <key name="const">$(devel.basic1).sn3.defs.sns3.sns3.type RStrong 2 0</key>
+    <key name="const">$(devel.basic1).sty0.defs.sty0.sty0.type TStep 4 0</key>
+    <key name="const">$(devel.basic1).sty1.defs.sty1.sty1.type TStepS 4 0</key>
     <key name="const">$(devel.basic1).subst0.defs.subst0.subst0.type Subst 4 0</key>
     <key name="const">$(devel.basic1).subst1.defs.subst1.subst1.type SubstS 4 0</key>
     <key name="const">$(devel.basic1).subst.defs.subst.subst.type FunSubstS 3 0</key>
@@ -285,12 +283,12 @@ $(devel.basic1).tlist.defs.THeads.THeads.type 0</key>
     <key name="const">$(devel.basic1).tlt.defs.wadd.type CoConsA 2 0</key>
     <key name="const">$(devel.basic1).tlt.defs.weight_map.weight_map.type CoWeightB 2 0</key>
     <key name="const">$(devel.basic1).tlt.defs.weight.type CoWeightA 1 0</key>
+    <key name="const">$(devel.basic1).ty3.defs.ty3.ty3.type Type 4 0</key>
+    <key name="const">$(devel.basic1).ty3.defs.tys3.tys3.type Type 4 0</key>
 <!--
-$(devel.basic1).ty3.defs.ty3.ty3.type 0</key>
-$(devel.basic1).ty3.defs.tys3.tys3.type 0</key>
 $(devel.basic1).ty3.nf2.ty3_nf2_inv_abst_premise.type 0</key>
-$(devel.basic1).wcpr0.defs.wcpr0.wcpr0.type 0</key>
-$(devel.basic1).wf3.defs.wf3.wf3.type 0</key>
 -->
+    <key name="const">$(devel.basic1).wcpr0.defs.wcpr0.wcpr0.type RStep 2 0</key>
+    <key name="const">$(devel.basic1).wf3.defs.wf3.wf3.type Valid 3 0</key>
   </section>
 </helm_registry>
diff --git a/matita/components/binaries/matex/test/basic_1.sty b/matita/components/binaries/matex/test/basic_1.sty
index 4cf406698..27fbe98b2 100644
--- a/matita/components/binaries/matex/test/basic_1.sty
+++ b/matita/components/binaries/matex/test/basic_1.sty
@@ -1,5 +1,5 @@
 \NeedsTeXFormat{LaTeX2e}[1995/12/01]
-\ProvidesPackage{basic_1}[2016/06/21 Notation for "cic:/matita/lambdadelta/basic_1/"]
+\ProvidesPackage{basic_1}[2016/06/24 Notation for "cic:/matita/lambdadelta/basic_1/"]
 \RequirePackage{legacy_1}
 \RequirePackage{ground_1}
 \ExecuteOptions{}
@@ -13,7 +13,12 @@
 \newcommand*\ld@cb[1]{\mathopen{]}}
 \newcommand*\ld@oB[1]{\mathopen{\lBrack}}
 \newcommand*\ld@cB[1]{\mathopen{\rBrack}}
+\newcommand*\ld@env[1]{\mathrel{\vdash}}
 
+\newcommand*\ld@arity[2]{\setrellink{\mathsf{arity}}{#1}{#2}}
+\newcommand*\ld@coconverts[1]{\setrellink{\mathsf{convert}_{\mathord\oplusrhrim}^*}{#1}{}}
+\newcommand*\ld@convert[1]{\setrellink{\mathsf{convert}}{#1}{}}
+\newcommand*\ld@converts[1]{\setrellink{\mathsf{convert}^*}{#1}{}}
 \newcommand*\ld@coweight[1]{\setoplink{\equivVvert}{#1}{}}
 \newcommand*\ld@drop[2]{\setoplink{\Downarrow}{#1}{#2}}
 \newcommand*\ld@drops[2]{\setoplink{\Downarrow^*}{#1}{#2}}
@@ -22,6 +27,7 @@
 \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@in[1]{\setrellink{\in}{#1}{}}
 \newcommand*\ld@leaf[1]{\setoplink{\star}{#1}{}}
 \newcommand*\ld@length@open[1]{\setopenlink{\vert}{#1}}
 \newcommand*\ld@length@close[1]{\setcloselink{\vert}{#1}}
@@ -29,19 +35,32 @@
 \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@rcandidate[2]{\setoplink{\mathsf{r\_candidate}}{#1}{#2}}
+\newcommand*\ld@rnormal[1]{\setoplink{\mathsf{r\_normal}}{#1}{}}
+\newcommand*\ld@rstep[1]{\setrellink{\mathsf{r\_step}}{#1}{}}
+\newcommand*\ld@rsteps[1]{\setrellink{\mathsf{r\_step^*}}{#1}{}}
+\newcommand*\ld@rstrong[1]{\setoplink{\mathsf{r\_strong}}{#1}{}}
 \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@tstep[2]{\setrellink{\mathsf{t\_step}}{#1}{#2}}
+\newcommand*\ld@tsteps[2]{\setrellink{\mathsf{t\_step^*}}{#1}{#2}}
+\newcommand*\ld@type[2]{\setrellink{\mathsf{type}}{#1}{#2}}
+\newcommand*\ld@valid[2]{\setoplink{\mathsf{valid}}{#1}{#2}}
 \newcommand*\ld@weight[1]{\setoplink{\equalparallel}{#1}{}}
 
 \newcommand*\ld@tuple@a[2]{\ld@oa{#1}#2\ld@ca{#1}}
 
+\newcommand*\Arity[5]{#3\ld@env{#1}#4\ld@arity{#1}{\ld@tuple@a{#1}{#2}}#5}
 \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*\CoConvertS[4]{#2\ld@env{#1}#3\ld@coconverts{#1}#4}
 \newcommand*\ConsA[3]{#2\ld@cons{#1}#3}
+\newcommand*\Convert[4]{#2\ld@env{#1}#3\ld@convert{#1}#4}
+\newcommand*\ConvertS[4]{#2\ld@env{#1}#3\ld@converts{#1}#4}
 \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}
@@ -61,12 +80,23 @@
 \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*\RCandidate[5]{\ld@tuple@b{#1}{#3}{#4}\ld@in{#1}\ld@rcandidate{#1}{\ld@tuple@a{#1}{#2}}#5}
+\newcommand*\RNormal[3]{#2\ld@env{#1}\ld@rnormal{#1}#3}
+\newcommand*\RStep[3]{#2\ld@rstep{#1}#3}
+\newcommand*\RStepA[4]{#2\ld@env{#1}#3\ld@rstep{#1}#4}
+\newcommand*\RStepS[3]{#2\ld@rsteps{#1}#3}
+\newcommand*\RStepSA[4]{#2\ld@env{#1}#3\ld@rsteps{#1}#4}
+\newcommand*\RStrong[3]{#2\ld@env{#1}\ld@rstrong{#1}#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*\TStep[5]{#3\ld@env{#1}#4\ld@tstep{#1}{\ld@tuple@a{#1}{#2}}#5}
+\newcommand*\TStepS[5]{#3\ld@env{#1}#4\ld@tsteps{#1}{\ld@tuple@a{#1}{#2}}#5}
+\newcommand*\Type[5]{#3\ld@env{#1}#4\ld@type{#1}{\ld@tuple@a{#1}{#2}}#5}
+\newcommand*\Valid[4]{\ld@valid{#1}{\ld@tuple@a{#1}{#2}}#3\ld@eq{#1}#4}
 \newcommand*\WeightA[2]{\ld@weight{#1}\ld@tuple@a{#1}{#2}}
 \newcommand*\WeightB[3]{\ld@weight{#1}\ld@tuple@b{#1}{#2}{#3}}