- 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 :)

diff --git a/helm/software/components/content_pres/boxPp.ml b/helm/software/components/content_pres/boxPp.ml
index bdd97a5e64aa5c3dbe6d275ab1ea0451ef3de5e3..0d58d97643a17aa147d117d006ed4cc8cec212d5 100644 (file)
--- 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 3d4ad9893ff791ea73267a15520c2566c906726a..328274bb8926de9989bf1a4fa43bd788ff294ebf 100644 (file)
--- 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 799841d7098bf883892f2304ef3f60b5ac0bd98d..33368a32d4bb8dc198e4fbdb395326faa49438c6 100644 (file)
--- 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 e594b82205d0423a05bc607bd5adb87615adefeb..bfa5112bc4f2d6482ef1f83a912df96359fd0b88 100644 (file)
--- 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.