- matex: minor improvements

- latex stylesheets: more notation for basic_1
  now we use just the stix fonts

diff --git a/matita/components/binaries/matex/Makefile b/matita/components/binaries/matex/Makefile
index c9a7b58ed7155b1a640dde8451431c23e79325ee..b3cc515d2ef748a01192eedb789efdb38fad7816 100644 (file)
--- a/matita/components/binaries/matex/Makefile
+++ b/matita/components/binaries/matex/Makefile
@@ -21,6 +21,6 @@ test/$(OBJS): $(REGISTRY)
 
 test/$(SRCS): test/$(OBJS) $(REGISTRY) ./matex.native
        @echo MaTeX: processing $<
-       $(H)./matex.native -O test -l $(SRCS) -p -g -a $(REGISTRY) `cat $<`
+       $(H)./matex.native -O test -l $(SRCS) -a -g -p $(REGISTRY) `cat $<`
 
 .PHONY: test

diff --git a/matita/components/binaries/matex/alpha.ml b/matita/components/binaries/matex/alpha.ml
index 4c4eccef70c0a81fad22842244f41547d10ea80f..6420d20c67d92fbb563efa8a08b89fe1cd334a0d 100644 (file)
--- a/matita/components/binaries/matex/alpha.ml
+++ b/matita/components/binaries/matex/alpha.ml
@@ -165,7 +165,7 @@ and proc_terms st ts =
 let proc_named_term s st t =
 try
    let tt = proc_term st t in
-   if !G.test then begin
+   if !G.check then begin
       let _ = K.typeof st.c tt in
       ok s
    end;

diff --git a/matita/components/binaries/matex/anticipate.ml b/matita/components/binaries/matex/anticipate.ml
index e6f51e55413ae3f391f413a7152fe2675265ef11..645d7b4170f19e2d628fc775512c721863d180ee 100644 (file)
--- a/matita/components/binaries/matex/anticipate.ml
+++ b/matita/components/binaries/matex/anticipate.ml
@@ -104,7 +104,7 @@ let shift_named_term s c t =
 try
    fresh := 0;
    let tt = shift_term c t in
-   if !G.test then begin
+   if !G.check then begin
       let _ = K.typeof c tt in
       ok s
    end;

diff --git a/matita/components/binaries/matex/engine.ml b/matita/components/binaries/matex/engine.ml
index 2fffd264ce1e416d1b1f324ea3ccf7fa0e2b21f8..83de453f733993275e73d7024a037015b8e3fc77 100644 (file)
--- a/matita/components/binaries/matex/engine.ml
+++ b/matita/components/binaries/matex/engine.ml
@@ -43,8 +43,8 @@ let internal s =
 let malformed s =
    X.error ("engine: malformed term: " ^ s)
 
-let missing s =
-   X.log ("engine: missing macro for " ^ s)
+let missing s l =
+   X.log (P.sprintf "engine: missing macro for %s (%u)" s l)
 
 (* generic term processing *)
 
@@ -72,13 +72,16 @@ let get_macro s l =
 let get_head = function
    | C.Const c :: ts ->
       let s, _ = K.resolve_reference c in
-      let macro, x = get_macro s (L.length ts) in
-      if macro <> "" then
-         let ts1, ts2 = X.split_at x ts in
-         Some (macro, s, ts1, ts2)
-      else begin 
-         if !G.log_missing then missing s;
-         None
+      let l = L.length ts in
+      let macro, x = get_macro s l in
+      begin match macro with      
+         | ""     -> 
+            if !G.log_missing then missing s l;
+            None
+         | "APPL" -> None
+         | _      -> 
+            let ts1, ts2 = X.split_at x ts in
+            Some (macro, s, ts1, ts2) 
       end 
    | _               -> None
 
@@ -243,6 +246,7 @@ let proc_item item s ss t =
    note :: T.Macro "begin" :: T.arg item :: T.arg (mk_gname s) :: T.free ss :: proc_term st is tt
 
 let proc_top_proof s ss t =
+   if !G.no_proofs then [] else
    let st = init ss in
    let t0 = A.process_top_term s t in  (* anticipation *)
    let tt = N.process_top_term s t0 in (* alpha-conversion *)

diff --git a/matita/components/binaries/matex/matex.ml b/matita/components/binaries/matex/matex.ml
index 88ae85436d3c06379b5973fb59104fe0a1b90387..ddd41304914bc1ba7235391c4668b1153c1d18e9 100644 (file)
--- a/matita/components/binaries/matex/matex.ml
+++ b/matita/components/binaries/matex/matex.ml
@@ -25,11 +25,12 @@ module K = Kernel
 let help_O = "<dir> Set this output directory"
 let help_X = " Clear configuration and options"
 let help_a = " Log alpha-unconverted identifiers (default: no)"
+let help_c = " Check term transformations (default: no)"
 let help_g = " Global alpha-conversion (default: no)"
 let help_l = "<file> Output the list of generated files in this file"
 let help_m = " Log missing notational macros (default: no)"
-let help_p = " Omit types (default: no)"
-let help_t = " Test term transformations (default: no)"
+let help_p = " Omit proofs (default: no)"
+let help_t = " Omit types (default: no)"
 
 let help   = ""
 
@@ -77,11 +78,12 @@ begin try
       "-O", A.String ((:=) G.out_dir), help_O;
       "-X", A.Unit G.clear, help_X;
       "-a", A.Set G.log_alpha, help_a;
+      "-c", A.Set G.check, help_c;
       "-g", A.Set G.global_alpha, help_g;
       "-l", A.String set_list, help_l;
       "-m", A.Set G.log_missing, help_m;
-      "-p", A.Set G.no_types, help_p;
-      "-t", A.Set G.test, help_t;
+      "-p", A.Set G.no_proofs, help_p;
+      "-t", A.Set G.no_types, help_t;
    ] process help
 with
    | X.Error s -> X.log s

diff --git a/matita/components/binaries/matex/options.ml b/matita/components/binaries/matex/options.ml
index b361841c608f8f13cc28d3e3d2759d86d716a5af..165b2d9784cce5310ccca448dd5207b1deab33ec 100644 (file)
--- a/matita/components/binaries/matex/options.ml
+++ b/matita/components/binaries/matex/options.ml
@@ -22,10 +22,12 @@ let default_out_dir = F.current_dir_name
 
 let default_proc_id = "H"
 
-let default_test = false
+let default_check = false
 
 let default_no_types = false
 
+let default_no_proofs = false
+
 let default_global_alpha = false
 
 let default_log_alpha = false
@@ -52,10 +54,12 @@ let out_dir = ref default_out_dir           (* directory of generated files *)
 
 let proc_id = ref default_proc_id           (* identifer for anticipations *)
 
-let test = ref default_test                 (* test anticipation *)
+let check = ref default_check               (* check transformations *)
 
 let no_types = ref default_no_types         (* omit types *)
 
+let no_proofs = ref default_no_proofs       (* omit proofs *)
+
 let global_alpha = ref default_global_alpha (* log alpha-unconverted identifiers *)
 
 let log_alpha = ref default_log_alpha       (* log alpha-unconverted identifiers *)
@@ -84,8 +88,9 @@ let clear () =
    no_init := default_no_init;
    out_dir := default_out_dir;
    proc_id := default_proc_id;
-   test := default_test;
+   check := default_check;
    no_types := default_no_types;
+   no_proofs := default_no_proofs;
    global_alpha := default_global_alpha;
    log_alpha := default_log_alpha;
    log_missing := default_log_missing;

diff --git a/matita/components/binaries/matex/options.mli b/matita/components/binaries/matex/options.mli
index 3801a8d19b1483d24841827e2412bb25cf75832d..1c6aef077bb61e42fb6ef735c126ae4a664189c4 100644 (file)
--- a/matita/components/binaries/matex/options.mli
+++ b/matita/components/binaries/matex/options.mli
@@ -21,10 +21,12 @@ val out_dir: string ref
 
 val proc_id: string ref
 
-val test: bool ref 
+val check: bool ref 
 
 val no_types: bool ref 
 
+val no_proofs: bool ref 
+
 val global_alpha: bool ref
 
 val log_alpha: bool ref

diff --git a/matita/components/binaries/matex/test/basic_1.conf.xml b/matita/components/binaries/matex/test/basic_1.conf.xml
index 5056ebfbca81c3077d59e8ff6bfc94e94546eb47..162425ddd7fc2dede898c25423222b091a44a87a 100644 (file)
--- a/matita/components/binaries/matex/test/basic_1.conf.xml
+++ b/matita/components/binaries/matex/test/basic_1.conf.xml
@@ -170,50 +170,60 @@
     <key name="gref">ty3_nf2_gen__ty3_nf2_inv_abst_aux ty3_nf2_inv_abst_aux</key>
   </section>
   <section name="matex.notation">
+    <key name="const">$(devel.basic1).A.defs.A.AHead.type To 2 0</key>
+    <key name="const">$(devel.basic1).A.defs.A.ASort.type AtomB 2 0</key>
 <!--
-$(devel.basic1).A.defs.A.AHead.type 0</key>
-$(devel.basic1).A.defs.A.ASort.type 0</key>
 $(devel.basic1).A.fwd.A_rect.A_rect.type 0</key>
 $(devel.basic1).aplus.defs.aplus.aplus.type 0</key>
-$(devel.basic1).app.defs.app1.app1.type 0</key>
-$(devel.basic1).app.defs.cbk.cbk.type 0</key>
+-->
+    <key name="const">$(devel.basic1).app.defs.app1.app1.type Shift 2 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>
 $(devel.basic1).asucc.defs.asucc.asucc.type 0</key>
 $(devel.basic1).C.defs.C.CHead.type 0</key>
-$(devel.basic1).C.defs.C.CSort.type 0</key>
-$(devel.basic1).C.defs.cle.type 0</key>
-$(devel.basic1).C.defs.clt.type 0</key>
+-->
+    <key name="const">$(devel.basic1).C.defs.C.CSort.type AtomA 1 0</key>
+    <key name="const">$(devel.basic1).C.defs.cle.type LE 2 0</key>
+    <key name="const">$(devel.basic1).C.defs.clt.type LT 2 0</key>
+<!--
 $(devel.basic1).C.defs.CTail.CTail.type 0</key>
-$(devel.basic1).C.defs.cweight.cweight.type 0</key>
+-->
+    <key name="const">$(devel.basic1).C.defs.cweight.cweight.type WeightA 1 0</key>
+<!--
 $(devel.basic1).C.fwd.C_rect.C_rect.type 0</key>
 $(devel.basic1).cimp.defs.cimp.type 0</key>
-$(devel.basic1).clear.defs.clear.clear.type 0</key>
-$(devel.basic1).clen.defs.clen.clen.type 0</key>
-$(devel.basic1).cnt.defs.cnt.cnt.type 0</key>
+-->
+    <key name="const">$(devel.basic1).clear.defs.clear.clear.type Drop 2 0</key>
+    <key name="const">$(devel.basic1).clen.defs.clen.clen.type Length 1 0</key>
+    <key name="const">$(devel.basic1).cnt.defs.cnt.cnt.type LEnv 1 0</key>
+<!--
 $(devel.basic1).csuba.defs.csuba.csuba.type 0</key>
 $(devel.basic1).csubc.defs.csubc.csubc.type 0</key>
-$(devel.basic1).csubst0.defs.csubst0.csubst0.type 0</key>
-$(devel.basic1).csubst1.defs.csubst1.csubst1.type 0</key>
+-->
+    <key name="const">$(devel.basic1).csubst0.defs.csubst0.csubst0.type Subst 4 0</key>
+    <key name="const">$(devel.basic1).csubst1.defs.csubst1.csubst1.type SubstS 4 0</key>
+<!--
 $(devel.basic1).csubt.defs.csubt.csubt.type 0</key>
 $(devel.basic1).csubv.defs.csubv.csubv.type 0</key>
 -->
-    <key name="const">$(devel.basic1).drop1.defs.drop1.drop1.type DropS 2 0</key>
+    <key name="const">$(devel.basic1).drop1.defs.drop1.drop1.type DropS 3 0</key>
 <!--
 $(devel.basic1).drop1.defs.ptrans.ptrans.type 0</key>
 -->
-    <key name="const">$(devel.basic1).drop.defs.drop.drop.type Drop 3 0</key>
+    <key name="const">$(devel.basic1).drop.defs.drop.drop.type DropB 4 0</key>
+    <key name="const">$(devel.basic1).ex0.defs.leqz.leqz.type Equiv 2 0</key>
+    <key name="const">$(devel.basic1).flt.defs.flt.type LTB 4 0</key>
+    <key name="const">$(devel.basic1).flt.defs.fweight.type WeightB 2 0</key>
+    <key name="const">$(devel.basic1).fsubst0.defs.fsubst0.fsubst0.type SubstB 6 0</key>
 <!--
-$(devel.basic1).ex0.defs.leqz.leqz.type 0</key>
-$(devel.basic1).flt.defs.flt.type 0</key>
-$(devel.basic1).flt.defs.fweight.type 0</key>
-$(devel.basic1).fsubst0.defs.fsubst0.fsubst0.type 0</key>
 $(devel.basic1).G.defs.G.mk_G.type 0</key>
-$(devel.basic1).G.defs.next.next.type 0</key>
-$(devel.basic1).getl.defs.getl.getl.type 0</key>
-$(devel.basic1).iso.defs.iso.iso.type 0</key>
-$(devel.basic1).leq.defs.leq.leq.type 0</key>
 -->
+    <key name="const">$(devel.basic1).G.defs.next.next.type Next 2 0</key>
+    <key name="const">$(devel.basic1).getl.defs.getl.getl.type DropA 3 0</key>
+    <key name="const">$(devel.basic1).iso.defs.iso.iso.type SameTop 2 0</key>
+    <key name="const">$(devel.basic1).leq.defs.leq.leq.type EquivA 3 0</key>
     <key name="const">$(devel.basic1).lift1.defs.lift1.lift1.type FunLiftS 2 0</key>
     <key name="const">$(devel.basic1).lift1.defs.lifts1.lifts1.type FunLiftS 2 0</key>
 <!--
@@ -221,10 +231,10 @@ $(devel.basic1).lift1.defs.trans.trans.type 0</key>
 -->
     <key name="const">$(devel.basic1).lift.defs.lifts.lifts.type FunLift 3 0</key>
     <key name="const">$(devel.basic1).lift.defs.lift.type FunLift 3 0</key>
+    <key name="const">$(devel.basic1).lift.defs.lref_map.lref_map.type FunLift 3 0</key>
+    <key name="const">$(devel.basic1).llt.defs.llt.type LT 2 0</key>
+    <key name="const">$(devel.basic1).llt.defs.lweight.lweight.type WeightA 1 0</key>
 <!--
-$(devel.basic1).lift.defs.lref_map.lref_map.type 0</key>
-$(devel.basic1).llt.defs.llt.type 0</key>
-$(devel.basic1).llt.defs.lweight.lweight.type 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>
@@ -235,37 +245,47 @@ $(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>
-$(devel.basic1).r.defs.r.type 0</key>
+-->
+    <key name="const">$(devel.basic1).r.defs.r.type FunW 2 0</key>
+<!--
 $(devel.basic1).sc3.defs.sc3.sc3.type 0</key>
-$(devel.basic1).s.defs.s.type 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>
-$(devel.basic1).subst0.defs.subst0.subst0.type 0</key>
-$(devel.basic1).subst1.defs.subst1.subst1.type 0</key>
-$(devel.basic1).subst.defs.subst.subst.type 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>
+<!--
 $(devel.basic1).T.defs.K.Bind.type 0</key>
 $(devel.basic1).T.defs.K.Flat.type 0</key>
-$(devel.basic1).T.defs.tle.type 0</key>
+-->
+    <key name="const">$(devel.basic1).T.defs.tle.type LE 2 0</key>
+<!--
 $(devel.basic1).T.defs.T.THead.type 0</key>
-$(devel.basic1).T.defs.T.TLRef.type 0</key>
-$(devel.basic1).T.defs.T.TSort.type 0</key>
-$(devel.basic1).T.defs.tweight.tweight.type 0</key>
+-->
+    <key name="const">$(devel.basic1).T.defs.T.TLRef.type LRef 1 0</key>
+    <key name="const">$(devel.basic1).T.defs.T.TSort.type AtomA 1 0</key>
+    <key name="const">$(devel.basic1).T.defs.tweight.tweight.type WeightA 1 0</key>
+<!--
 $(devel.basic1).T.fwd.T_rect.T_rect.type 0</key>
 -->
-    <key name="const">$(devel.basic1).tlist.defs.TApp.TApp.type RevConsA 2 0</key>
+    <key name="const">$(devel.basic1).tlist.defs.TApp.TApp.type CoConsA 2 0</key>
 <!--
 $(devel.basic1).tlist.defs.THeads.THeads.type 0</key>
 -->
     <key name="const">$(devel.basic1).tlist.defs.TList.TCons.type ConsA 2 0</key>
+    <key name="const">$(devel.basic1).tlist.defs.tslen.tslen.type Length 1 0</key>
+    <key name="const">$(devel.basic1).tlist.defs.tslt.type LT 2 0</key>
+    <key name="const">$(devel.basic1).tlt.defs.tlt.type LT 2 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>
 <!--
-$(devel.basic1).tlist.defs.tslen.tslen.type 0</key>
-$(devel.basic1).tlist.defs.tslt.type 0</key>
-$(devel.basic1).tlt.defs.tlt.type 0</key>
-$(devel.basic1).tlt.defs.wadd.type 0</key>
-$(devel.basic1).tlt.defs.weight_map.weight_map.type 0</key>
-$(devel.basic1).tlt.defs.weight.type 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>

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
 

diff --git a/matita/components/binaries/matex/test/ground_1.conf.xml b/matita/components/binaries/matex/test/ground_1.conf.xml
index 3c5fab2212088aff3733a01d150734a9e299ab3d..ec9676bb4888c4829848d8d34f7aea4b4972dc4d 100644 (file)
--- a/matita/components/binaries/matex/test/ground_1.conf.xml
+++ b/matita/components/binaries/matex/test/ground_1.conf.xml
@@ -25,7 +25,7 @@
 
     <key name="const">$(devel.ground1).blt.defs.blt.blt.type FunLt 2 0</key>
     <key name="const">$(devel.ground1).plist.defs.papp.papp.type Append 2 0</key>
-    <key name="const">$(devel.ground1).plist.defs.PConsTail.PConsTail.type RevConsB 3 0</key>
+    <key name="const">$(devel.ground1).plist.defs.PConsTail.PConsTail.type CoConsB 3 0</key>
     <key name="const">$(devel.ground1).plist.defs.PList.PCons.type ConsB 3 0</key>
     <key name="const">$(devel.ground1).plist.defs.Ss.Ss.type Succ 1 0</key>
   </section>

diff --git a/matita/components/binaries/matex/test/ground_1.sty b/matita/components/binaries/matex/test/ground_1.sty
index e1da3f4af9773e348b53aa990da777b4c41d8787..c641d59efcf9f78109b145bd14a0bdaea3a8e67e 100644 (file)
--- a/matita/components/binaries/matex/test/ground_1.sty
+++ b/matita/components/binaries/matex/test/ground_1.sty
@@ -1,8 +1,6 @@
 \NeedsTeXFormat{LaTeX2e}[1995/12/01]
-\ProvidesPackage{ground_1}[2016/06/19 Notation for "cic:/matita/lambdadelta/ground_1/"]
+\ProvidesPackage{ground_1}[2016/06/21 Notation for "cic:/matita/lambdadelta/ground_1/"]
 \RequirePackage{matex}
-\let\bigtimes\undefined
-\RequirePackage{mathabx}
 \ExecuteOptions{}
 \ProcessOptions*
 
@@ -12,17 +10,17 @@
 \newcommand*\ld@oa[1]{\mathopen{\langle}}
 \newcommand*\ld@ca[1]{\mathclose{\rangle}}
 
-\newcommand*\ld@append[1]{\setbinlink{\oplus}{#1}}
-\newcommand*\ld@cons[1]{\setbinlink{\oright}{#1}}
-\newcommand*\ld@funlt[1]{\setbinlink{\olessthan}{#1}}
-\newcommand*\ld@revcons[1]{\setbinlink{\oleft}{#1}}
+\newcommand*\ld@append[1]{\setbinlink{\oplus}{#1}{}}
+\newcommand*\ld@cocons[1]{\setbinlink{\opluslhrim}{#1}{}}
+\newcommand*\ld@cons[1]{\setbinlink{\oplusrhrim}{#1}{}}
+\newcommand*\ld@funlt[1]{\setbinlink{\olessthan}{#1}{}}
 
 \newcommand*\ld@tuple@b[3]{\ld@oa{#1}#2\ld@cm{#1}#3\ld@ca{#1}}
 
 \newcommand*\Append[3]{#2\ld@append{#1}#3}
+\newcommand*\CoConsB[4]{#2\ld@cocons{#1}\ld@tuple@b{#1}{#3}{#4}}
 \newcommand*\ConsB[4]{\ld@tuple@b{#1}{#2}{#3}\ld@cons{#1}#4}
 \newcommand*\FunLt[3]{#2\ld@funlt{#1}#3}
-\newcommand*\RevConsB[4]{#2\ld@revcons{#1}\ld@tuple@b{#1}{#3}{#4}}
 
 \makeatother
 

diff --git a/matita/components/binaries/matex/test/legacy_1.sty b/matita/components/binaries/matex/test/legacy_1.sty
index 45d3199cb4b7074d8e415d8b3d649e4817813fb7..f7dd9382b603ac252500165b99eb41910008c8ac 100644 (file)
--- a/matita/components/binaries/matex/test/legacy_1.sty
+++ b/matita/components/binaries/matex/test/legacy_1.sty
@@ -1,5 +1,5 @@
 \NeedsTeXFormat{LaTeX2e}[1995/12/01]
-\ProvidesPackage{legacy_1}[2016/06/19 Notation for "cic:/matita/lambdadelta/legacy_1/"]
+\ProvidesPackage{legacy_1}[2016/06/21 Notation for "cic:/matita/lambdadelta/legacy_1/"]
 \RequirePackage{matex}
 \ExecuteOptions{}
 \ProcessOptions*
@@ -8,19 +8,19 @@
 
 \makeatletter
 
-\newcommand*\ld@and[1]{\setbinlink{\&}{#1}}
+\newcommand*\ld@and[1]{\setbinlink{\&}{#1}{}}
 \newcommand*\ld@lex[1]{\setordlink{\exists}{#1}}
-\newcommand*\ld@land[1]{\setrellink{\land}{#1}}
-\newcommand*\ld@lor[1]{\setrellink{\lor}{#1}}
-
-\newcommand*\ld@eq[1]{\setrellink{=}{#1}}
-\newcommand*\ld@le[1]{\setrellink{\le}{#1}}
-\newcommand*\ld@lt[1]{\setrellink{<}{#1}}
-\newcommand*\ld@minus[1]{\setbinlink{-}{#1}}
-\newcommand*\ld@lnot[1]{\setoplink{\lnot}{#1}}
-\newcommand*\ld@plus[1]{\setbinlink{+}{#1}}
-\newcommand*\ld@pred[1]{\setoplink{\midcir}{#1}}
-\newcommand*\ld@succ[1]{\setoplink{\cirmid}{#1}}
+\newcommand*\ld@land[1]{\setrellink{\land}{#1}{}}
+\newcommand*\ld@lor[1]{\setrellink{\lor}{#1}{}}
+
+\newcommand*\ld@eq[1]{\setrellink{=}{#1}{}}
+\newcommand*\ld@le[1]{\setrellink{\le}{#1}{}}
+\newcommand*\ld@lt[1]{\setrellink{<}{#1}{}}
+\newcommand*\ld@minus[1]{\setbinlink{-}{#1}{}}
+\newcommand*\ld@lnot[1]{\setoplink{\lnot}{#1}{}}
+\newcommand*\ld@plus[1]{\setbinlink{+}{#1}{}}
+\newcommand*\ld@pred[1]{\setoplink{\midcir}{#1}{}}
+\newcommand*\ld@succ[1]{\setoplink{\cirmid}{#1}{}}
 
 \newcommand*\ld@list[2]{\ma@list\relax\ma@arg{#1{#2}}\relax}
 

diff --git a/matita/components/binaries/matex/test/matex.sty b/matita/components/binaries/matex/test/matex.sty
index a46b2af1b264840cca78e867e0dd9ac02f67f283..b01223fefec60774fc182dabebde22033d01edea 100644 (file)
--- a/matita/components/binaries/matex/test/matex.sty
+++ b/matita/components/binaries/matex/test/matex.sty
@@ -1,7 +1,7 @@
 \NeedsTeXFormat{LaTeX2e}[1995/12/01]
-\ProvidesPackage{matex}[2016/06/19 MaTeX Package]
+\ProvidesPackage{matex}[2016/06/21 MaTeX Package]
 \RequirePackage{xcolor}
-\RequirePackage{stix}
+\RequirePackage[lcgreekalpha]{stix}
 \ExecuteOptions{}
 \ProcessOptions*
 
@@ -44,12 +44,12 @@
 }
 
 \newcommand*\setordlink[2]{\mathord{\ma@setlink{#1}{#2}}}
-\newcommand*\setoplink[2]{\mathop{\ma@setlink{#1}{#2}}}
-\newcommand*\setbinlink[2]{\mathbin{\ma@setlink{#1}{#2}}}
-\newcommand*\setrellink[2]{\mathrel{\ma@setlink{#1}{#2}}}
 \newcommand*\setopenlink[2]{\mathopen{\ma@setlink{#1}{#2}}}
 \newcommand*\setcloselink[2]{\mathclose{\ma@setlink{#1}{#2}}}
 \newcommand*\setpunctlink[2]{\mathpunct{\ma@setlink{#1}{#2}}}
+\newcommand*\setoplink[3]{\mathop{\ma@setlink{#1}{#2}#3}}
+\newcommand*\setbinlink[3]{\mathbin{\ma@setlink{#1}{#2}#3}}
+\newcommand*\setrellink[3]{\mathrel{\ma@setlink{#1}{#2}#3}}
 
 \newcommand*\ObjIncNode{}
 \newcommand*\ObjNode{}

diff --git a/matita/components/binaries/matex/test/test.tex b/matita/components/binaries/matex/test/test.tex
index 26adf2224ff385a5201954da57a06f817553ddb1..0cf2e639fe774755dec155cb79b8b51bba482a43 100644 (file)
--- a/matita/components/binaries/matex/test/test.tex
+++ b/matita/components/binaries/matex/test/test.tex
@@ -1,5 +1,6 @@
-\documentclass[8pt,twocolumn]{extarticle}
+\documentclass[8pt,twocolumn,a4paper]{extarticle}
 
+\usepackage[margin=2cm]{geometry}
 \usepackage[bookmarks=false,ps2pdf]{hyperref}
 \usepackage[american]{babel}
 \usepackage{matex}
@@ -11,7 +12,8 @@
 \renewcommand*\ObjIncNode{\stepcounter{node}}
 \renewcommand*\ObjNode{\arabic{node} }
 
-\title{The Core Theory of the Formal System $\lambda\delta\hbox{-}1$}
+\title{The Core Theory of the Formal System $\lambda\delta\hbox{-}1$:
+Definitions and Statements}
 
 \author{Ferruccio Guidi}