better, reparsable, notation

diff --git a/helm/software/components/content_pres/boxPp.ml b/helm/software/components/content_pres/boxPp.ml
index a51920c799416b2db97b3e7e22ee4196ffbefd1a..bdd97a5e64aa5c3dbe6d275ab1ea0451ef3de5e3 100644 (file)
--- a/helm/software/components/content_pres/boxPp.ml
+++ b/helm/software/components/content_pres/boxPp.ml
@@ -185,6 +185,7 @@ let render_to_strings ~map_unicode_to_tex choose_action size markup =
   and aux_mpres =
     let text s = Pres.Mtext ([], s) in
     let mrow c = Pres.Mrow ([], c) in
+    let parentesize s = s in
     function
     | Pres.Mi (_, s)
     | Pres.Mn (_, s)
@@ -209,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("; text ")"; text "("; n; text ")" ])
-    | Pres.Msqrt (_, m) -> aux_mpres (mrow [ text "\\sqrt("; m; text ")" ])
+       aux_mpres (mrow [ text " \\frac "; parentesize m ; parentesize n])
+    | Pres.Msqrt (_, m) -> aux_mpres (mrow [ text " \\sqrt "; parentesize m; ])
     | Pres.Mroot (_, r, i) ->
         aux_mpres (mrow [
-          text "\\root("; i; text ")"; text "\\of("; r; text ")" ])
+          text " \\root "; parentesize i; text " \\of "; parentesize r ])
     | Pres.Mstyle (_, m)
     | Pres.Merror (_, m)
     | Pres.Mpadded (_, m)
@@ -222,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 [ text "("; m; text ")\\sub("; n; text ")" ])
+        aux_mpres (mrow [ parentesize m; text " \\sub "; parentesize n ])
     | Pres.Msup (_, m, n) ->
-        aux_mpres (mrow [ text "("; m; text ")\\sup("; n; text ")" ])
+        aux_mpres (mrow [ parentesize m; text " \\sup "; parentesize n ])
     | Pres.Munder (_, m, n) ->
-        aux_mpres (mrow [ text "("; m; text ")\\below("; n; text ")" ])
+        aux_mpres (mrow [ parentesize m; text " \\below "; parentesize n ])
     | Pres.Mover (_, m, n) ->
-        aux_mpres (mrow [ text "("; m; text ")\\above("; n; text ")" ])
+        aux_mpres (mrow [ parentesize m; text " \\above "; parentesize n ])
     | Pres.Msubsup _
     | Pres.Munderover _
     | Pres.Mtable _ ->

diff --git a/helm/software/matita/contribs/dama/dama/models/q_function.ma b/helm/software/matita/contribs/dama/dama/models/q_function.ma
index 48d3012ec66974d8c8993e5db02bd72e3b488229..0d34f2cebd904ca53d4daaeed59676ac0bf41904 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/models/q_function.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_function.ma
@@ -91,6 +91,7 @@ definition inject ≝
 (*coercion inject with 0 1 nocomposites.*)
 coercion cic:/matita/dama/models/q_function/inject.con 0 1 nocomposites.
 
+(* a local letin makes russell fail *)
 definition cb0h ≝ (λl.mk_list (λi.〈\fst (nth l q0 i),OQ〉) (length ? l)).
 
 alias symbol "pi2" = "pair pi2".
@@ -118,17 +119,17 @@ match n with
          let height1 ≝ (\snd he1) in
          let height2 ≝ (\snd he2) in
          match q_cmp base1 base2 with
-         [ q_eq _ ⇒
+         [ q_eq _ ⇒ 〈[],[]〉 (*
              let rc ≝ aux tl1 tl2 m in 
-             〈he1 :: \fst rc,he2 :: \snd rc〉
-         | q_lt _ ⇒ 
+             〈he1 :: \fst rc,he2 :: \snd rc〉 *)
+         | q_lt _ ⇒ 〈[],[]〉 (*
              let rest ≝ base2 - base1 in
              let rc ≝ aux tl1 (〈rest,height2〉 :: tl2) m in
-             〈〈base1,height1〉 :: \fst rc,〈base1,height2〉 :: \snd rc〉
-         | q_gt _ ⇒ 
+             〈〈base1,height1〉 :: \fst rc,〈base1,height2〉 :: \snd rc〉 *)
+         | q_gt _ ⇒ 〈[],[]〉 (*
              let rest ≝ base1 - base2 in
              let rc ≝ aux (〈rest,height1〉 :: tl1) tl2 m in
-             〈〈base2,height1〉 :: \fst rc,〈base2,height2〉 :: \snd rc〉
+             〈〈base2,height1〉 :: \fst rc,〈base2,height2〉 :: \snd rc〉 *)
 ]]]]
 in aux : ∀l1,l2,m.∃z.spec l1 l2 m z); 
 qed.
\ No newline at end of file

diff --git a/helm/software/matita/contribs/dama/dama/sequence.ma b/helm/software/matita/contribs/dama/dama/sequence.ma
index d3acf437ff68684cc089044582fd29c1ad81800e..948d14f67963ef2e929bba924e40edbe58572ea4 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/sequence.ma
+++ b/helm/software/matita/contribs/dama/dama/sequence.ma
@@ -31,7 +31,7 @@ for @{ 'sequence (\lambda ${ident i} . $p)}.
 notation > "hvbox(\lfloor ident i, term 19 p \rfloor)" with precedence 90
 for @{ 'sequence (\lambda ${ident i} . $p)}.
   
-notation "a \sub i" left associative with precedence 70 
+notation "a \sub i" left associative with precedence 90 
   for @{ 'sequence_appl $a $i }.
 
 interpretation "sequence" 'sequence \eta.x = (mk_seq _ x).

diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo
index c6e3d6015c61ef563ef48f0daf02c18a2a48cbbc..9055293175f66328f4719569dfa7d1c142ecdc74 100644 (file)
--- a/helm/software/matita/core_notation.moo
+++ b/helm/software/matita/core_notation.moo
@@ -10,14 +10,14 @@ with precedence 90 for @{ 'pair $a $b}.
 notation "hvbox(x break \times y)" with precedence 70
 for @{ 'product $x $y}.
 
-notation < "\fst \nbsp x" non associative with precedence 69 for @{'pi1a $x}.
-notation < "\snd \nbsp x" non associative with precedence 69 for @{'pi2a $x}.
+notation < "\fst \nbsp term 90 x" with precedence 69 for @{'pi1a $x}.
+notation < "\snd \nbsp term 90 x" with precedence 69 for @{'pi2a $x}.
 
-notation < "\fst \nbsp x \nbsp y" non associative with precedence 69 for @{'pi1b $x $y}.
-notation < "\snd \nbsp x \nbsp y" non associative with precedence 69 for @{'pi2b $x $y}.
+notation < "\fst \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi1b $x $y}.
+notation < "\snd \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi2b $x $y}.
 
-notation > "\fst" non associative with precedence 90 for @{'pi1}.
-notation > "\snd" non associative with precedence 90 for @{'pi2}.
+notation > "\fst" with precedence 90 for @{'pi1}.
+notation > "\snd" with precedence 90 for @{'pi2}.
 
 notation "hvbox(a break \to b)" 
   right associative with precedence 20