From b4a67321811bdc123636eaa0f117d5308cb7a07b Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 3 Jun 2009 20:20:11 +0000 Subject: [PATCH] - boxPp: added missing spaces - core_notation: bug fix in the input notation for congruent: we added term 90 after \sub - library/nat/permutation.ma: added input notation for transpose and fixed term precedence in its output notation - library/Makefile: compilation of single files re-enabled. The syntax for compiling file.ma is is "make file.mo" and "make file.mo.opt" now nat/congruence.ma and nat/permutation.ma are fully reconstructed :) --- helm/software/components/content_pres/boxPp.ml | 14 +++++++------- helm/software/matita/core_notation.moo | 2 +- helm/software/matita/library/Makefile | 5 +++++ helm/software/matita/library/nat/permutation.ma | 9 ++++++--- 4 files changed, 19 insertions(+), 11 deletions(-) diff --git a/helm/software/components/content_pres/boxPp.ml b/helm/software/components/content_pres/boxPp.ml index bdd97a5e6..0d58d9764 100644 --- a/helm/software/components/content_pres/boxPp.ml +++ b/helm/software/components/content_pres/boxPp.ml @@ -210,11 +210,11 @@ let render_to_strings ~map_unicode_to_tex choose_action size markup = let children' = List.map aux_mpres children in (fun size -> render_row size false children') | Pres.Mfrac (_, m, n) -> - aux_mpres (mrow [ text " \\frac "; parentesize m ; parentesize n]) - | Pres.Msqrt (_, m) -> aux_mpres (mrow [ text " \\sqrt "; parentesize m; ]) + aux_mpres (mrow [ text " \\frac "; parentesize m ; text " "; parentesize n; text " " ]) + | Pres.Msqrt (_, m) -> aux_mpres (mrow [ text " \\sqrt "; parentesize m; text " "]) | Pres.Mroot (_, r, i) -> aux_mpres (mrow [ - text " \\root "; parentesize i; text " \\of "; parentesize r ]) + text " \\root "; parentesize i; text " \\of "; parentesize r; text " " ]) | Pres.Mstyle (_, m) | Pres.Merror (_, m) | Pres.Mpadded (_, m) @@ -223,13 +223,13 @@ let render_to_strings ~map_unicode_to_tex choose_action size markup = | Pres.Mfenced (_, children) -> aux_mpres (mrow children) | Pres.Maction (_, []) -> assert false | Pres.Msub (_, m, n) -> - aux_mpres (mrow [ parentesize m; text " \\sub "; parentesize n ]) + aux_mpres (mrow [ text " "; parentesize m; text " \\sub "; parentesize n; text " " ]) | Pres.Msup (_, m, n) -> - aux_mpres (mrow [ parentesize m; text " \\sup "; parentesize n ]) + aux_mpres (mrow [ text " "; parentesize m; text " \\sup "; parentesize n; text " " ]) | Pres.Munder (_, m, n) -> - aux_mpres (mrow [ parentesize m; text " \\below "; parentesize n ]) + aux_mpres (mrow [ text " "; parentesize m; text " \\below "; parentesize n; text " " ]) | Pres.Mover (_, m, n) -> - aux_mpres (mrow [ parentesize m; text " \\above "; parentesize n ]) + aux_mpres (mrow [ text " "; parentesize m; text " \\above "; parentesize n; text " " ]) | Pres.Msubsup _ | Pres.Munderover _ | Pres.Mtable _ -> diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo index 3d4ad9893..328274bb8 100644 --- a/helm/software/matita/core_notation.moo +++ b/helm/software/matita/core_notation.moo @@ -62,7 +62,7 @@ notation < "hvbox(term 46 a break maction (=) (=\sub t) term 46 b)" non associative with precedence 45 for @{ 'eq $t $a $b }. -notation > "hvbox(n break (≅ \sub p) m)" +notation > "hvbox(n break (≅ \sub term 90 p) m)" non associative with precedence 45 for @{ 'congruent $n $m $p }. diff --git a/helm/software/matita/library/Makefile b/helm/software/matita/library/Makefile index 799841d70..33368a32d 100644 --- a/helm/software/matita/library/Makefile +++ b/helm/software/matita/library/Makefile @@ -12,3 +12,8 @@ depend: ../matitadep -dot depend.opt: ../matitadep.opt -dot + +%.mo: + ../matitac $*.ma +%.mo.opt: + ../matitac.opt $*.ma diff --git a/helm/software/matita/library/nat/permutation.ma b/helm/software/matita/library/nat/permutation.ma index e594b8220..bfa5112bc 100644 --- a/helm/software/matita/library/nat/permutation.ma +++ b/helm/software/matita/library/nat/permutation.ma @@ -72,10 +72,13 @@ match eqb n i with [ true \Rightarrow i | false \Rightarrow n]]. -notation < "(❲i↹j❳)n" with precedence 71 +notation < "(❲i↹j❳) term 72 n" with precedence 71 for @{ 'transposition $i $j $n}. -notation < "(❲i \atop j❳)n" with precedence 71 +notation < "(❲i \atop j❳) term 72 n" with precedence 71 +for @{ 'transposition $i $j $n}. + +notation > "(❲\frac term 90 i term 90 j❳)n" with precedence 71 for @{ 'transposition $i $j $n}. interpretation "natural transposition" 'transposition i j n = (transpose i j n). @@ -747,4 +750,4 @@ intros 4.elim k ] ] ] -qed. \ No newline at end of file +qed. -- 2.39.2