partial notational update in ground_2 and basic_2 ....

+ the notation for lists and streams contains a bug

diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
index 03ea90426fdb1ed9b37a8ecd0f2237f6177db03d..51f54e6e3b8dad8158d2291fa13f522ec0bd6ed6 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -232,7 +232,7 @@ table {
           }
         ]
         [ { "append" * } {
-             [ [ "for lenvs" ] "append" + "( ? @@ ? )" "append_length" * ]
+             [ [ "for lenvs" ] "append" + "( ? + ? )" "append_length" * ]
           }
         ]
         [ { "head equivalence" * } {

diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_2.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_2.ma
deleted file mode 100644 (file)
index c95c57d..0000000
--- a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_2.ma
+++ /dev/null
@@ -1,19 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
-
-notation "hvbox( hd @ break tl )"
-  right associative with precedence 47
-  for @{ 'Cons $hd $tl }.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_3.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_3.ma
deleted file mode 100644 (file)
index cfa556e..0000000
--- a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_3.ma
+++ /dev/null
@@ -1,19 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
-
-notation "hvbox( { term 46 hd1 , break term 46 hd2 } @ break term 46 tl )"
-  non associative with precedence 47
-  for @{ 'Cons $hd1 $hd2 $tl }.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/oplusright_3.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/oplusright_3.ma
new file mode 100644 (file)
index 0000000..e172f4a
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/oplusright_3.ma
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation < "hvbox( hd ⨮ break tl )"
+  right associative with precedence 47
+  for @{ 'OPlusRight $S $hd $tl }.
+
+notation > "hvbox( hd ⨮ break tl )"
+  right associative with precedence 47
+  for @{ 'OPlusRight ? $hd $tl }.
+
+notation > "hvbox( hd ⨮{ break term 46 S } break term 46 tl )"
+  non associative with precedence 47
+  for @{ 'OPlusRight $S $hd $tl }.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/oplusright_5.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/oplusright_5.ma
new file mode 100644 (file)
index 0000000..6da02ad
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/oplusright_5.ma
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation < "hvbox( { term 46 hd1, break term 46 hd2 }⨮ break term 46 tl )"
+  non associative with precedence 47
+  for @{ 'OplusRight $S1 $S2 $hd1 $hd2 $tl }.
+
+notation > "hvbox( { term 46 hd1, break term 46 hd2 }⨮ break term 46 tl )"
+  non associative with precedence 47
+  for @{ 'OplusRight ? ? $hd1 $hd2 $tl }.
+(*
+(**) fix pair notation
+notation > "hvbox( { term 46 hd1, break term 46 hd2 }⨮{ break term 46 S1, break term 46 S2 } break term 46 tl )"
+  non associative with precedence 47
+  for @{ 'OplusRight $S1 $S2 $hd1 $hd2 $tl }.
+*)

diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index e51f7b54eba7d77cf98588122a588407b8efcec5..02a5c226998cf2db2d032370d45219c133f591a6 100644 (file)
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1510,7 +1510,7 @@ let predefined_classes = [
  [":"; "⁝"; ];
  ["."; "•"; "◦"; ];
  ["#"; "♯"; "⋕"; "⧣"; "⧤"; "⌘"; ];
- ["+"; "⊕"; "⊞"; ];
+ ["+"; "⨭"; "⨮"; "â\8a\95"; "â\8a\9e"; ];
  ["-"; "÷"; "⊢"; "⊩"; "⧟"; "⊟"; ];
  ["="; "≝"; "≡"; "≘"; "≗"; "≐"; "≑"; "≛"; "≚"; "≙"; "⌆"; "⧦"; "⊜"; "≋"; "⩳"; "≅"; "⩬"; "≂"; "≃"; "≈"; ];  
  ["→"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "⤳"; ] ;