From: Ferruccio Guidi Date: Tue, 1 May 2018 22:56:24 +0000 (+0200) Subject: partial notational update in ground_2 and basic_2 .... X-Git-Tag: make_still_working~334 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=b598b37379baabef24ae511596be7f740cbb0c2e 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 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/cons_2.ma deleted file mode 100644 index c95c57d8e..000000000 --- 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 index cfa556e68..000000000 --- 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 index 000000000..e172f4abe --- /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 index 000000000..6da02adc1 --- /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 e51f7b54e..02a5c2269 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1510,7 +1510,7 @@ let predefined_classes = [ [":"; "⁝"; ]; ["."; "•"; "◦"; ]; ["#"; "♯"; "⋕"; "⧣"; "⧤"; "⌘"; ]; - ["+"; "⊕"; "⊞"; ]; + ["+"; "⨭"; "⨮"; "⊕"; "⊞"; ]; ["-"; "÷"; "⊢"; "⊩"; "⧟"; "⊟"; ]; ["="; "≝"; "≡"; "≘"; "≗"; "≐"; "≑"; "≛"; "≚"; "≙"; "⌆"; "⧦"; "⊜"; "≋"; "⩳"; "≅"; "⩬"; "≂"; "≃"; "≈"; ]; ["→"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "⤳"; ] ;