From a221802803194112119f727b0911be4fba069b27 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 25 Jun 2008 09:11:34 +0000 Subject: [PATCH] better, reparsable, notation --- helm/software/components/content_pres/boxPp.ml | 15 ++++++++------- .../contribs/dama/dama/models/q_function.ma | 13 +++++++------ .../matita/contribs/dama/dama/sequence.ma | 2 +- helm/software/matita/core_notation.moo | 12 ++++++------ 4 files changed, 22 insertions(+), 20 deletions(-) diff --git a/helm/software/components/content_pres/boxPp.ml b/helm/software/components/content_pres/boxPp.ml index a51920c79..bdd97a5e6 100644 --- 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 48d3012ec..0d34f2ceb 100644 --- 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 d3acf437f..948d14f67 100644 --- 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 c6e3d6015..905529317 100644 --- 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 -- 2.39.2