From b598b37379baabef24ae511596be7f740cbb0c2e Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 2 May 2018 00:56:24 +0200
Subject: [PATCH] partial notational update in ground_2 and basic_2 ....

+ the notation for lists and streams contains a bug
---
 .../lambdadelta/basic_2/web/basic_2_src.tbl        |  2 +-
 .../constructors/{cons_2.ma => oplusright_3.ma}    | 12 ++++++++++--
 .../constructors/{cons_3.ma => oplusright_5.ma}    | 14 ++++++++++++--
 matita/matita/predefined_virtuals.ml               |  2 +-
 4 files changed, 24 insertions(+), 6 deletions(-)
 rename matita/matita/contribs/lambdadelta/ground_2/notation/constructors/{cons_2.ma => oplusright_3.ma} (77%)
 rename matita/matita/contribs/lambdadelta/ground_2/notation/constructors/{cons_3.ma => oplusright_5.ma} (68%)

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 03ea90426..51f54e6e3 100644
--- 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/oplusright_3.ma
similarity index 77%
rename from matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_2.ma
rename to matita/matita/contribs/lambdadelta/ground_2/notation/constructors/oplusright_3.ma
index c95c57d8e..e172f4abe 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_2.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/oplusright_3.ma
@@ -14,6 +14,14 @@
 
 (* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
 
-notation "hvbox( hd @ break tl )"
+notation < "hvbox( hd ⨮ break tl )"
   right associative with precedence 47
-  for @{ 'Cons $hd $tl }.
+  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/cons_3.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/oplusright_5.ma
similarity index 68%
rename from matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_3.ma
rename to matita/matita/contribs/lambdadelta/ground_2/notation/constructors/oplusright_5.ma
index cfa556e68..6da02adc1 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_3.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/oplusright_5.ma
@@ -14,6 +14,16 @@
 
 (* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
 
-notation "hvbox( { term 46 hd1 , break term 46 hd2 } @ break term 46 tl )"
+notation < "hvbox( { term 46 hd1, break term 46 hd2 }⨮ break term 46 tl )"
   non associative with precedence 47
-  for @{ 'Cons $hd1 $hd2 $tl }.
+  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 e51f7b54e..02a5c2269 100644
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1510,7 +1510,7 @@ let predefined_classes = [
  [":"; "⁝"; ];
  ["."; "•"; "◦"; ];
  ["#"; "♯"; "⋕"; "⧣"; "⧤"; "⌘"; ];
- ["+"; "⊕"; "⊞"; ];
+ ["+"; "⨭"; "⨮"; "⊕"; "⊞"; ];
  ["-"; "÷"; "⊢"; "⊩"; "⧟"; "⊟"; ];
  ["="; "≝"; "≡"; "≘"; "≗"; "≐"; "≑"; "≛"; "≚"; "≙"; "⌆"; "⧦"; "⊜"; "≋"; "⩳"; "≅"; "⩬"; "≂"; "≃"; "≈"; ];  
  ["→"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "⤳"; ] ;
-- 
2.39.2