From f1f80d3696cca276a0e07babe46debd2447007f7 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 29 May 2009 14:26:50 +0000 Subject: [PATCH] - cicNotationParser: added extra space to TeX control sequences accordind to previous commit of cicNotationLexer - core_notation: bugfix in the notation for exp - library/nat/congruence.ma: notation for "congruent" moved to core_notation now nat/exp.ma is fully reconstructed :) --- .../content_pres/cicNotationParser.ml | 44 +++++++++---------- helm/software/matita/core_notation.moo | 28 ++++++++---- .../software/matita/library/nat/congruence.ma | 6 +-- 3 files changed, 43 insertions(+), 35 deletions(-) diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml index 695db149e..bb3d29f06 100644 --- a/helm/software/components/content_pres/cicNotationParser.ml +++ b/helm/software/components/content_pres/cicNotationParser.ml @@ -170,18 +170,18 @@ let extract_term_production pattern = [NoBinding, gram_keyword s] | `Number s -> [NoBinding, gram_number s] and aux_layout = function - | Ast.Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sub"] @ aux p2 - | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sup"] @ aux p2 - | Ast.Below (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\below"] @ aux p2 - | Ast.Above (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\above"] @ aux p2 - | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\frac"] @ aux p2 - | Ast.InfRule (p1, p2, p3) -> [NoBinding, gram_symbol "\\infrule"] @ aux p1 @ aux p2 @ aux p3 - | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\atop"] @ aux p2 - | Ast.Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\over"] @ aux p2 + | Ast.Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sub "] @ aux p2 + | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sup "] @ aux p2 + | Ast.Below (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\below "] @ aux p2 + | Ast.Above (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\above "] @ aux p2 + | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\frac "] @ aux p2 + | Ast.InfRule (p1, p2, p3) -> [NoBinding, gram_symbol "\\infrule "] @ aux p1 @ aux p2 @ aux p3 + | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\atop "] @ aux p2 + | Ast.Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\over "] @ aux p2 | Ast.Root (p1, p2) -> - [NoBinding, gram_symbol "\\root"] @ aux p2 - @ [NoBinding, gram_symbol "\\of"] @ aux p1 - | Ast.Sqrt p -> [NoBinding, gram_symbol "\\sqrt"] @ aux p + [NoBinding, gram_symbol "\\root "] @ aux p2 + @ [NoBinding, gram_symbol "\\of "] @ aux p1 + | Ast.Sqrt p -> [NoBinding, gram_symbol "\\sqrt "] @ aux p | Ast.Break -> [] | Ast.Box (_, pl) -> List.flatten (List.map aux pl) | Ast.Group pl -> List.flatten (List.map aux pl) @@ -460,33 +460,33 @@ EXTEND v = [ PERCENTAGE ] -> id, v]]; l1_simple_pattern: [ "layout" LEFTA - [ p1 = SELF; SYMBOL "\\sub"; p2 = SELF -> + [ p1 = SELF; SYMBOL "\\sub "; p2 = SELF -> return_term_of_level loc (fun l -> Ast.Layout (Ast.Sub (p1 l, p2 l))) - | p1 = SELF; SYMBOL "\\sup"; p2 = SELF -> + | p1 = SELF; SYMBOL "\\sup "; p2 = SELF -> return_term_of_level loc (fun l -> Ast.Layout (Ast.Sup (p1 l, p2 l))) - | p1 = SELF; SYMBOL "\\below"; p2 = SELF -> + | p1 = SELF; SYMBOL "\\below "; p2 = SELF -> return_term_of_level loc (fun l -> Ast.Layout (Ast.Below (p1 l, p2 l))) - | p1 = SELF; SYMBOL "\\above"; p2 = SELF -> + | p1 = SELF; SYMBOL "\\above "; p2 = SELF -> return_term_of_level loc (fun l -> Ast.Layout (Ast.Above (p1 l, p2 l))) - | p1 = SELF; SYMBOL "\\over"; p2 = SELF -> + | p1 = SELF; SYMBOL "\\over "; p2 = SELF -> return_term_of_level loc (fun l -> Ast.Layout (Ast.Over (p1 l, p2 l))) - | p1 = SELF; SYMBOL "\\atop"; p2 = SELF -> + | p1 = SELF; SYMBOL "\\atop "; p2 = SELF -> return_term_of_level loc (fun l -> Ast.Layout (Ast.Atop (p1 l, p2 l))) - | p1 = SELF; SYMBOL "\\frac"; p2 = SELF -> + | p1 = SELF; SYMBOL "\\frac "; p2 = SELF -> return_term_of_level loc (fun l -> Ast.Layout (Ast.Frac (p1 l, p2 l))) - | SYMBOL "\\infrule"; p1 = SELF; p2 = SELF; p3 = SELF -> + | SYMBOL "\\infrule "; p1 = SELF; p2 = SELF; p3 = SELF -> return_term_of_level loc (fun l -> Ast.Layout (Ast.InfRule (p1 l, p2 l, p3 l))) - | SYMBOL "\\sqrt"; p = SELF -> + | SYMBOL "\\sqrt "; p = SELF -> return_term_of_level loc (fun l -> Ast.Layout (Ast.Sqrt p l)) - | SYMBOL "\\root"; index = SELF; SYMBOL "\\of"; arg = SELF -> + | SYMBOL "\\root "; index = SELF; SYMBOL "\\of "; arg = SELF -> return_term_of_level loc (fun l -> Ast.Layout (Ast.Root (arg l, index l))) | "hbox"; LPAREN; p = l1_pattern; RPAREN -> @@ -588,7 +588,7 @@ EXTEND ] ]; explicit_subst: [ - [ SYMBOL "\\subst"; (* to avoid catching frequent "a [1]" cases *) + [ SYMBOL "\\subst "; (* to avoid catching frequent "a [1]" cases *) SYMBOL "["; substs = LIST1 [ i = IDENT; SYMBOL <:unicode> (* ≔ *); t = term -> (i, t) diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo index ae589803f..3d4ad9893 100644 --- a/helm/software/matita/core_notation.moo +++ b/helm/software/matita/core_notation.moo @@ -52,6 +52,24 @@ notation > "\Sigma list1 ident x sep , opt (: T). term 19 Px" @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}.$acc)} } } }. +(* equality, conguence ******************************************************) + +notation > "hvbox(a break = b)" + non associative with precedence 45 +for @{ 'eq ? $a $b }. + +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)" + non associative with precedence 45 +for @{ 'congruent $n $m $p }. + +notation < "hvbox(term 46 n break ≅ \sub p term 46 m)" + non associative with precedence 45 +for @{ 'congruent $n $m $p }. + (* other notations **********************************************************) notation "hvbox(\langle term 19 a, break term 19 b\rangle)" @@ -77,13 +95,6 @@ notation < "hvbox(a break \to b)" right associative with precedence 20 for @{ \Pi $_:$a.$b }. -notation > "hvbox(a break = b)" - non associative with precedence 45 -for @{ 'eq ? $a $b }. -notation < "hvbox(term 46 a break maction (=) (=\sub t) term 46 b)" - non associative with precedence 45 -for @{ 'eq $t $a $b }. - notation "hvbox(a break \leq b)" non associative with precedence 45 for @{ 'leq $a $b }. @@ -247,7 +258,8 @@ notation "↑a" with precedence 55 for @{ 'uparrow $a }. notation "hvbox(a break ↑ b)" with precedence 55 for @{ 'funion $a $b }. -notation "a \sup term 89 b" with precedence 90 for @{ 'exp $a $b}. +notation < "term 91 a \sup term 90 b" with precedence 90 for @{ 'exp $a $b}. +notation > "a \sup term 89 b" with precedence 90 for @{ 'exp $a $b}. notation > "a ^ term 89 b" with precedence 90 for @{ 'exp $a $b}. notation "s \sup (-1)" with precedence 90 for @{ 'invert $s }. notation > "s ^ (-1)" with precedence 90 for @{ 'invert $s }. diff --git a/helm/software/matita/library/nat/congruence.ma b/helm/software/matita/library/nat/congruence.ma index 4266d3f6f..0a635ff78 100644 --- a/helm/software/matita/library/nat/congruence.ma +++ b/helm/software/matita/library/nat/congruence.ma @@ -1,5 +1,5 @@ (**************************************************************************) -(* ___ *) +(* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) @@ -23,10 +23,6 @@ definition congruent: nat \to nat \to nat \to Prop \def interpretation "congruent" 'congruent n m p = (congruent n m p). -notation < "hvbox(n break \cong\sub p m)" - (*non associative*) with precedence 45 -for @{ 'congruent $n $m $p }. - theorem congruent_n_n: \forall n,p:nat.congruent n n p. intros.unfold congruent.reflexivity. qed. -- 2.39.2