From bedea63520c165e9445c15b09455e349c72e48a5 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 3 Jul 2016 22:16:54 +0000 Subject: [PATCH] - matex: we separate axioms (propositions) and assumptions (other) - matex.sty: some improvements including color for metalinguistic term constructions - stylesheets: some improvements including more notation for basic_1 --- matita/components/binaries/matex/engine.ml | 8 ++- .../binaries/matex/test/basic_1.conf.xml | 66 ++++++----------- .../binaries/matex/test/basic_1.sty | 39 ++++++++-- .../binaries/matex/test/legacy_1.sty | 10 +-- .../components/binaries/matex/test/matex.sty | 71 +++++++++++-------- .../components/binaries/matex/test/test.tex | 2 +- 6 files changed, 106 insertions(+), 90 deletions(-) diff --git a/matita/components/binaries/matex/engine.ml b/matita/components/binaries/matex/engine.ml index 83de453f7..c3d50d5e7 100644 --- a/matita/components/binaries/matex/engine.ml +++ b/matita/components/binaries/matex/engine.ml @@ -262,10 +262,14 @@ let open_out_tex s = open_out (F.concat !G.out_dir fname) let proc_pair s ss u = function - | None -> + | None -> + let text_u = + if K.not_prop1 [] u then proc_item "assumption" + else proc_item "axiom" + in let name = X.rev_map_concat X.id "." "type" ss in let och = open_out_tex name in - O.out_text och (proc_item "axiom" s name u); + O.out_text och (text_u s name u); close_out och | Some t -> let text_u, text_t = diff --git a/matita/components/binaries/matex/test/basic_1.conf.xml b/matita/components/binaries/matex/test/basic_1.conf.xml index 451e77ba5..10095057b 100644 --- a/matita/components/binaries/matex/test/basic_1.conf.xml +++ b/matita/components/binaries/matex/test/basic_1.conf.xml @@ -174,76 +174,58 @@ $(devel.basic1).A.defs.A.ASort.type AtomB 2 0 + $(devel.basic1).aplus.defs.aplus.aplus.type PlusA 3 0 $(devel.basic1).app.defs.app1.app1.type Shift 2 0 $(devel.basic1).app.defs.cbk.cbk.type Level 1 0 - + $(devel.basic1).aprem.defs.aprem.aprem.type CoPremise 3 0 $(devel.basic1).arity.defs.arity.arity.type Arity 4 0 - + $(devel.basic1).asucc.defs.asucc.asucc.type SuccA 2 0 + $(devel.basic1).C.defs.C.CHead.type LHead 3 0 $(devel.basic1).C.defs.C.CSort.type AtomA 1 0 $(devel.basic1).C.defs.cle.type LE 2 0 $(devel.basic1).C.defs.clt.type LT 2 0 - + $(devel.basic1).C.defs.CTail.CTail.type THead 3 0 $(devel.basic1).C.defs.cweight.cweight.type WeightA 1 0 + $(devel.basic1).cimp.defs.cimp.type SubEq 2 0 $(devel.basic1).clear.defs.clear.clear.type Drop 2 0 $(devel.basic1).clen.defs.clen.clen.type Length 1 0 $(devel.basic1).cnt.defs.cnt.cnt.type LEnv 1 0 - + $(devel.basic1).csuba.defs.csuba.csuba.type LSupA 3 0 + $(devel.basic1).csubc.defs.csubc.csubc.type LSupC 3 0 $(devel.basic1).csubst0.defs.csubst0.csubst0.type Subst 4 0 $(devel.basic1).csubst1.defs.csubst1.csubst1.type SubstS 4 0 - + $(devel.basic1).csubt.defs.csubt.csubt.type LSupT 3 0 + $(devel.basic1).csubv.defs.csubv.csubv.type LSup 2 0 $(devel.basic1).drop1.defs.drop1.drop1.type DropS 3 0 - + $(devel.basic1).drop1.defs.ptrans.ptrans.type ApplS 2 0 $(devel.basic1).drop.defs.drop.drop.type DropB 4 0 $(devel.basic1).ex0.defs.leqz.leqz.type Equiv 2 0 $(devel.basic1).flt.defs.flt.type LTB 4 0 $(devel.basic1).flt.defs.fweight.type WeightB 2 0 $(devel.basic1).fsubst0.defs.fsubst0.fsubst0.type SubstB 6 0 - + $(devel.basic1).G.defs.G.mk_G.type MkSH 2 0 $(devel.basic1).G.defs.next.next.type Next 2 0 $(devel.basic1).getl.defs.getl.getl.type DropA 3 0 $(devel.basic1).iso.defs.iso.iso.type SameTop 2 0 $(devel.basic1).leq.defs.leq.leq.type EquivA 3 0 $(devel.basic1).lift1.defs.lift1.lift1.type FunLiftS 2 0 $(devel.basic1).lift1.defs.lifts1.lifts1.type FunLiftS 2 0 - + $(devel.basic1).lift1.defs.trans.trans.type Appl 2 0 $(devel.basic1).lift.defs.lifts.lifts.type FunLift 3 0 $(devel.basic1).lift.defs.lift.type FunLift 3 0 $(devel.basic1).lift.defs.lref_map.lref_map.type FunLift 3 0 $(devel.basic1).llt.defs.llt.type LT 2 0 $(devel.basic1).llt.defs.lweight.lweight.type WeightA 1 0 - + $(devel.basic1).next_plus.defs.next_plus.next_plus.type NextS 3 0 $(devel.basic1).nf2.defs.nf2.type RNormal 2 0 $(devel.basic1).nf2.defs.nfs2.nfs2.type RNormal 2 0 - $(devel.basic1).pc1.defs.pc1.type Convert 3 0 - $(devel.basic1).pc3.defs.pc3_left.pc3_left.type CoConvertS 3 0 - $(devel.basic1).pc3.defs.pc3.type ConvertS 3 0 + $(devel.basic1).pc1.defs.pc1.type ConvertS 2 0 + $(devel.basic1).pc3.defs.pc3_left.pc3_left.type CoConvertSA 3 0 + $(devel.basic1).pc3.defs.pc3.type ConvertSA 3 0 $(devel.basic1).pr0.defs.pr0.pr0.type RStep 2 0 $(devel.basic1).pr1.defs.pr1.pr1.type RStepS 2 0 $(devel.basic1).pr2.defs.pr2.pr2.type RStepA 3 0 @@ -258,14 +240,10 @@ $(devel.basic1).next_plus.defs.next_plus.next_plus.type 0 $(devel.basic1).subst0.defs.subst0.subst0.type Subst 4 0 $(devel.basic1).subst1.defs.subst1.subst1.type SubstS 4 0 $(devel.basic1).subst.defs.subst.subst.type FunSubstS 3 0 - + $(devel.basic1).T.defs.K.Bind.type Bind 1 0 + $(devel.basic1).T.defs.K.Flat.type Flat 1 0 $(devel.basic1).T.defs.tle.type LE 2 0 - + $(devel.basic1).T.defs.T.THead.type THead 3 0 $(devel.basic1).T.defs.T.TLRef.type LRef 1 0 $(devel.basic1).T.defs.T.TSort.type AtomA 1 0 $(devel.basic1).T.defs.tweight.tweight.type WeightA 1 0 @@ -273,9 +251,7 @@ $(devel.basic1).T.defs.T.THead.type 0 $(devel.basic1).T.fwd.T_rect.T_rect.type 0 --> $(devel.basic1).tlist.defs.TApp.TApp.type CoConsA 2 0 - + $(devel.basic1).tlist.defs.THeads.THeads.type THead 3 0 $(devel.basic1).tlist.defs.TList.TCons.type ConsA 2 0 $(devel.basic1).tlist.defs.tslen.tslen.type Length 1 0 $(devel.basic1).tlist.defs.tslt.type LT 2 0 diff --git a/matita/components/binaries/matex/test/basic_1.sty b/matita/components/binaries/matex/test/basic_1.sty index 27fbe98b2..71e48ff02 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/24 Notation for "cic:/matita/lambdadelta/basic_1/"] +\ProvidesPackage{basic_1}[2016/07/03 Notation for "cic:/matita/lambdadelta/basic_1/"] \RequirePackage{legacy_1} \RequirePackage{ground_1} \ExecuteOptions{} @@ -14,19 +14,25 @@ \newcommand*\ld@oB[1]{\mathopen{\lBrack}} \newcommand*\ld@cB[1]{\mathopen{\rBrack}} \newcommand*\ld@env[1]{\mathrel{\vdash}} +\newcommand*\ld@fs[1]{\mathord{.}} +\newcommand*\ld@appl[1]{\setbinlink{@}{#1}{}} +\newcommand*\ld@appls[1]{\setbinlink{\overline{@}}{#1}{}} \newcommand*\ld@arity[2]{\setrellink{\mathsf{arity}}{#1}{#2}} +\newcommand*\ld@bind[1]{\setordlink{\mathbf{B}}{#1}{}} \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@copremise[2]{\setoplink{\mathsf{copremise}}{#1}{#2}} \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@flat[1]{\setoplink{\mathbf{F}}{#1}{}} \newcommand*\ld@funlift[2]{\setoplink{\uparrow}{#1}{#2}} -\newcommand*\ld@funlifts[2]{\setoplink{\uparrow^*}{#1}{}} +\newcommand*\ld@funlifts[2]{\setoplink{\uparrow^*}{#1}{#2}} \newcommand*\ld@funv[2]{\setoplink{\mathsf{v}}{#1}{#2}} \newcommand*\ld@funw[2]{\setoplink{\mathsf{w}}{#1}{#2}} +\newcommand*\ld@pair[2]{\setordlink{\mathbf{P}}{#1}{#2}} \newcommand*\ld@in[1]{\setrellink{\in}{#1}{}} \newcommand*\ld@leaf[1]{\setoplink{\star}{#1}{}} \newcommand*\ld@length@open[1]{\setopenlink{\vert}{#1}} @@ -34,6 +40,10 @@ \newcommand*\ld@lenv[1]{\setoplink{\mathsf{lenv}}{#1}{}} \newcommand*\ld@level[1]{\setoplink{\mathsf{level}}{#1}{}} \newcommand*\ld@lref[1]{\setoplink{\#}{#1}{}} +\newcommand*\ld@lsup[2]{\setrellink{\sqsupseteq}{#1}{#2}} +\newcommand*\ld@lsupa[2]{\setrellink{\mathord\sqsupseteq\lozenge}{#1}{#2}} +\newcommand*\ld@lsupt[2]{\setrellink{\mathord\sqsupseteq\mathord:}{#1}{#2}} +\newcommand*\ld@mksh[1]{\setordlink{\mathbf{H}}{#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}{}} @@ -42,6 +52,7 @@ \newcommand*\ld@rstrong[1]{\setoplink{\mathsf{r\_strong}}{#1}{}} \newcommand*\ld@sametop[1]{\setrellink{\eqsim}{#1}{}} \newcommand*\ld@shift[1]{\setordlink{.}{#1}} +\newcommand*\ld@subeq[1]{\setrellink{\subseteq}{#1}{}} \newcommand*\ld@subst[1]{\setbinlink{/}{#1}{}} \newcommand*\ld@substs[1]{\setbinlink{/^*}{#1}{}} \newcommand*\ld@to[1]{\setrellink{\rightarrow}{#1}{}} @@ -53,14 +64,18 @@ \newcommand*\ld@tuple@a[2]{\ld@oa{#1}#2\ld@ca{#1}} +\newcommand*\Appl[3]{#2\ld@appl{#1}#3} +\newcommand*\ApplS[3]{#2\ld@appls{#1}#3} \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*\Bind[2]{\ld@bind{#1}\ld@tuple@a{#1}{#2}} \newcommand*\CoConsA[3]{#2\ld@cocons{#1}#3} -\newcommand*\CoConvertS[4]{#2\ld@env{#1}#3\ld@coconverts{#1}#4} +\newcommand*\CoConvertSA[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*\ConvertS[3]{#2\ld@converts{#1}#3} +\newcommand*\ConvertSA[4]{#2\ld@env{#1}#3\ld@converts{#1}#4} +\newcommand*\CoPremise[4]{\ld@copremise{#1}{\ld@tuple@a{#1}{#2}}#3\ld@eq{#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} @@ -69,6 +84,7 @@ \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*\Flat[2]{\ld@flat{#1}\ld@tuple@a{#1}{#2}} \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} @@ -77,9 +93,17 @@ \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*\LHead[4]{#2\ld@fs{#1}\ld@pair{#1}{\ld@tuple@a{#1}{#3}}#4} \newcommand*\LRef[2]{\ld@lref{#1}#2} +\newcommand*\LSup[3]{#2\ld@lsup{#1}{}#3} +\newcommand*\LSupA[4]{#3\ld@lsupa{#1}{\ld@tuple@a{#1}{#2}}#4} +\newcommand*\LSupC[4]{#3\ld@lsup{#1}{\ld@tuple@a{#1}{#2}}#4} +\newcommand*\LSupT[4]{#3\ld@lsupt{#1}{\ld@tuple@a{#1}{#2}}#4} \newcommand*\LTB[5]{\ld@tuple@b{#1}{#2}{#3}\ld@lt{#1}\ld@tuple@b{#1}{#4}{#5}} +\newcommand*\MkSH[3]{\ld@mksh{#1}\ld@tuple@b{#1}{#2}{#3}} \newcommand*\Next[3]{\ld@next{#1}{\ld@tuple@a{#1}{#2}}#3} +\newcommand*\NextS[4]{\ld@next{#1}{^{#4}\ld@tuple@a{#1}{#2}}#3} +\newcommand*\PlusA[4]{#3\ld@plus{#1}{\ld@tuple@a{#1}{#2}}#4} \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} @@ -89,9 +113,12 @@ \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*\SubEq[3]{#2\ld@subeq{#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*\SuccA[3]{\ld@succ{#1}{\ld@tuple@a{#1}{#2}}#3} +\newcommand*\THead[4]{\ld@pair{#1}{\ld@tuple@a{#1}{#2}}#3\ld@fs{#1}#4} \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} diff --git a/matita/components/binaries/matex/test/legacy_1.sty b/matita/components/binaries/matex/test/legacy_1.sty index f7dd9382b..b240c44b1 100644 --- 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/21 Notation for "cic:/matita/lambdadelta/legacy_1/"] +\ProvidesPackage{legacy_1}[2016/07/03 Notation for "cic:/matita/lambdadelta/legacy_1/"] \RequirePackage{matex} \ExecuteOptions{} \ProcessOptions* @@ -18,9 +18,9 @@ \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@plus[2]{\setbinlink{+}{#1}{#2}} \newcommand*\ld@pred[1]{\setoplink{\midcir}{#1}{}} -\newcommand*\ld@succ[1]{\setoplink{\cirmid}{#1}{}} +\newcommand*\ld@succ[2]{\setoplink{\cirmid}{#1}{#2}} \newcommand*\ld@list[2]{\ma@list\relax\ma@arg{#1{#2}}\relax} @@ -33,9 +33,9 @@ \newcommand*\LT[3]{#2\ld@lt{#1}#3} \newcommand*\Minus[3]{#2\ld@minus{#1}#3} \newcommand*\LNot[2]{\ld@lnot{#1}#2} -\newcommand*\Plus[3]{#2\ld@plus{#1}#3} +\newcommand*\Plus[3]{#2\ld@plus{#1}{}#3} \newcommand*\Pred[2]{\ld@pred{#1}#2} -\renewcommand*\Succ[2]{\ld@succ{#1}#2} +\renewcommand*\Succ[2]{\ld@succ{#1}{}#2} \makeatother diff --git a/matita/components/binaries/matex/test/matex.sty b/matita/components/binaries/matex/test/matex.sty index b01223fef..7d6ae277e 100644 --- a/matita/components/binaries/matex/test/matex.sty +++ b/matita/components/binaries/matex/test/matex.sty @@ -1,33 +1,43 @@ \NeedsTeXFormat{LaTeX2e}[1995/12/01] -\ProvidesPackage{matex}[2016/06/21 MaTeX Package] +\ProvidesPackage{matex}[2016/07/03 MaTeX Package] \RequirePackage{xcolor} \RequirePackage[lcgreekalpha]{stix} \ExecuteOptions{} \ProcessOptions* -\makeatletter +\newcommand*\neverindent{\setlength\parindent{0pt}} -\newcommand*\ma@cast{\mathbin:} -\newcommand*\ma@abbr{\mathrel\eqdef} -\newcommand*\ma@prod{\mathord\Pi} -\newcommand*\ma@arrw{\mathrel\Rightarrow} -\newcommand*\ma@fall{\mathord\forall} -\newcommand*\ma@impl{\mathrel\supset} -\newcommand*\ma@case{\mathrel\questeq} -\newcommand*\ma@caze{\mathrel\mapsto} -\newcommand*\ma@pair{\mathbin\mapsto} +\makeatletter \definecolor{ma@black}{HTML}{000000} \definecolor{ma@blue}{HTML}{00005F} \definecolor{ma@purple}{HTML}{3F005F} +\definecolor{ma@green}{HTML}{004F00} +\newcommand*\ma@punct{ma@green} \newcommand*\ma@fwd{ma@black} \newcommand*\ma@open{ma@blue} \newcommand*\ma@exit{ma@blue} \newcommand*\ma@prim{ma@purple} \newcommand*\ma@qed{ma@blue} -\newcommand*\neverindent{\setlength\parindent{0pt}} +\newcommand*\ma@constr[1]{{\color{\ma@punct}#1}} +\newcommand*\ma@thop[1]{\mathpunct{#1}\allowbreak} + +\newcommand*\ma@cast{\mathbin\ma@constr{:}} +\newcommand*\ma@abbr{\mathrel\ma@constr{\eqdef}} +\newcommand*\ma@prod{\mathord\ma@constr{\Pi}} +\newcommand*\ma@arrw{\mathrel\ma@constr{\Rightarrow}} +\newcommand*\ma@fall{\mathord\ma@constr{\forall}} +\newcommand*\ma@impl{\mathrel\ma@constr{\supset}} +\newcommand*\ma@case{\mathrel\ma@constr{\questeq}} +\newcommand*\ma@caze{\mathrel\ma@constr{\mapsto}} +\newcommand*\ma@pair{\mathbin\ma@constr{\mapsto}} +\newcommand*\ma@cm{\ma@thop{\ma@constr{,}}} +\newcommand*\ma@or{\mathbin\ma@constr{\vert}} +\newcommand*\ma@op{\mathopen\ma@constr{(}} +\newcommand*\ma@cp{\mathclose\ma@constr{)}\allowbreak} +\newcommand*\ma@qm{\mathord\ma@constr{?}} %\newcommand*\setlabel[1]{\protected@edef\@currentlabel{#1}} %\newcommand*\ObjLabel[1]{\label{obj:#1}\hypertarget{obj:#1}{}} @@ -54,14 +64,18 @@ \newcommand*\ObjIncNode{} \newcommand*\ObjNode{} -\newcommand*\ma@thehead[3]{\ObjIncNode\textbf{#1 \ObjNode(\ma@settarget{#2}{#3})}\neverindent\par} -\newcommand*\ma@theneck[1]{\textsl{#1}\neverindent\par} - -\newenvironment{axiom}[2]{\ma@thehead{Axiom}{#1}{#2}$}{$\par} -\newenvironment{declaration}[2]{\ma@thehead{Declaration}{#1}{#2}$}{$\par} -\newenvironment{definition}[2]{$}{$\par} -\newenvironment{proposition}[2]{\ma@thehead{Proposition}{#1}{#2}$}{$\par} -\newenvironment{proof}[2]{\ma@theneck{Proof}}{\par} +\newcommand*\ma@thehead[4]{\ObjIncNode + \textbf{#1 \ObjNode:} (\ma@settarget{#3}{#4}) \textit{#2:}% + \neverindent\par +} +\newcommand*\ma@theneck[1]{\textit{#1:}\neverindent\par} + +\newenvironment{assumption}[2]{\ma@thehead{Assumption}{has type}{#1}{#2}$}{$\par} +\newenvironment{axiom}[2]{\ma@thehead{Axiom}{states}{#1}{#2}$}{$\par} +\newenvironment{declaration}[2]{\ma@thehead{Definition}{of type}{#1}{#2}$}{$\par} +\newenvironment{definition}[2]{\ma@theneck{is defined as}$}{$\par} +\newenvironment{proposition}[2]{\ma@thehead{Proposition}{stating}{#1}{#2}$}{$\par} +\newenvironment{proof}[2]{\ma@theneck{is proved by}}{\par} \newenvironment{ma@step}[1]{\color{#1}}{\par} \newcommand*\ma@tmp{} @@ -70,13 +84,8 @@ \ifx\ma@tmp\empty\let\ma@tmp=\ma@last\else #1#2{#5}\let\ma@tmp=\ma@list\fi \ma@tmp{#3}{#2}{#3}{#4}% } -\newcommand*\ma@thop[1]{\mathpunct{#1}\allowbreak} -\newcommand*\ma@cm{\ma@thop{,}} -\newcommand*\ma@or{\mathbin\vert} -\newcommand*\ma@cp{)\allowbreak} -\newcommand*\ma@qm{\mathord{?}} \newcommand*\ma@arg[1]{#1} -\newcommand*\ma@args{(\ma@list\relax\ma@arg\ma@cm\ma@cp} +\newcommand*\ma@args{\ma@op\ma@list\relax\ma@arg\ma@cm\ma@cp} \newcommand*\ma@cases{\ma@list\relax\ma@arg\ma@or\relax} \newcommand*\ma@bind{\ma@thop{}} \newcommand*\ma@skip[1]{} @@ -86,19 +95,19 @@ \newcommand*\TYPE[1]{\mathord\mathrm{TYPE}} \newcommand*\LREF[2]{\ma@setoptlink{#1}{#2}} \newcommand*\GREF[2]{\ma@setoptlink{\mathrm{#1}}{#2}} -\newcommand*\ABBR[4]{(\ma@setopttarget{#1}{#2}\ma@abbr #4\ma@cast #3)\ma@bind} -\newcommand*\ABST[3]{(\ma@setopttarget{#1}{#2}\ma@cast #3)\ma@bind} +\newcommand*\ABBR[4]{\ma@op\ma@setopttarget{#1}{#2}\ma@abbr #4\ma@cast #3\ma@cp\ma@bind} +\newcommand*\ABST[3]{\ma@op\ma@setopttarget{#1}{#2}\ma@cast #3\ma@cp\ma@bind} \newcommand*\PROD[3]{\def\ma@tmp{#2}% \ifx\ma@tmp\empty #3\ma@arrw\else - (\ma@prod\ma@setopttarget{#1}{#2}\ma@cast #3)\ma@bind\fi + \ma@op\ma@prod\ma@setopttarget{#1}{#2}\ma@cast #3\ma@cp\ma@bind\fi } \newcommand*\FALL[3]{\def\ma@tmp{#2}% \ifx\ma@tmp\empty #3\ma@impl\else - (\ma@fall\ma@setopttarget{#1}{#2}\ma@cast #3)\ma@bind\fi + \ma@op\ma@fall\ma@setopttarget{#1}{#2}\ma@cast #3\ma@cp\ma@bind\fi } \newcommand*\APPL[1]{#1\ma@args} \newcommand*\CASE[3]{#3\ma@case\ma@cases} -\newcommand*\CAZE[3]{#3\ma@caze(\ma@qm\ma@cast #2)\ma@cases} +\newcommand*\CAZE[3]{#3\ma@caze\ma@op\ma@qm\ma@cast #2\ma@cp\ma@cases} \newcommand*\PAIR[2]{#1\ma@pair #2} \newcommand*\ma@term[1]{$#1$} diff --git a/matita/components/binaries/matex/test/test.tex b/matita/components/binaries/matex/test/test.tex index 0cf2e639f..a1591d4d5 100644 --- a/matita/components/binaries/matex/test/test.tex +++ b/matita/components/binaries/matex/test/test.tex @@ -10,7 +10,7 @@ \newcounter{node} \renewcommand*\ObjIncNode{\stepcounter{node}} -\renewcommand*\ObjNode{\arabic{node} } +\renewcommand*\ObjNode{\arabic{node}} \title{The Core Theory of the Formal System $\lambda\delta\hbox{-}1$: Definitions and Statements} -- 2.39.2