From: Ferruccio Guidi Date: Sun, 28 Feb 2021 21:32:01 +0000 (+0100) Subject: update in ground X-Git-Tag: make_still_working~153 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=77c9255de3c5f7780aeacd745703a1cc76328a68;p=helm.git update in ground + notation restyled --- diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/dGroundLib.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/dGroundLib.mrc index c829279fd..bb30f97e9 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/dGroundLib.mrc +++ b/matita/matita/contribs/lambdadelta/bin/recomm/dGroundLib.mrc @@ -1,5 +1,5 @@ PccFor d "" true false -GROUND NOTATION, GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ +GROUND NOTATION RELATIONS FUNCTIONS LOGIC diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundLib.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundLib.ml index 7fda12b7c..1adbf9894 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundLib.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundLib.ml @@ -12,7 +12,6 @@ let step k st outs ins = | "FUNCTIONS" :: tl -> k T.OK ("FUNCTIONS" :: outs) tl | "RELATIONS" :: tl -> k T.OK ("RELATIONS" :: outs) tl | "GROUND" :: "NOTATION" :: tl -> k T.OK ("NOTATION" :: "GROUND" :: outs) tl - | "GENERAL" :: "NOTATION" :: "USED" :: "BY" :: "THE" :: "FORMAL" :: "SYSTEM" :: "\206\187\206\180" :: tl -> k T.OK ("NOTATION" :: "GROUND" :: outs) tl | _ -> k T.OO outs ins let main = diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/append_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/append_2.ma index f6d95184b..acf8e6df2 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/append_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/append_2.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox( l1 @@ break l2 )" right associative with precedence 47 diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/apply_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/apply_2.ma index f770230c8..38d063225 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/apply_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/apply_2.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox( f @❨ break term 46 a ❩ )" non associative with precedence 60 diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/basic_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/basic_2.ma index 52ebf0ebd..fddd6406b 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/basic_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/basic_2.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox( 𝐁❨ term 46 l, break term 46 h ❩ )" non associative with precedence 90 diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/circledE_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/circledE_1.ma index 53cf85698..669db2e7a 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/circledE_1.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/circledE_1.ma @@ -12,16 +12,16 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation < "hvbox( Ⓔ )" - non associative with precedence 55 - for @{ 'CircledE $S }. + non associative with precedence 55 + for @{ 'CircledE $S }. notation > "hvbox( Ⓔ )" - non associative with precedence 55 - for @{ 'CircledE ? }. + non associative with precedence 55 + for @{ 'CircledE ? }. notation > "hvbox( Ⓔ{ term 46 C } )" - non associative with precedence 55 - for @{ 'CircledE $S }. + non associative with precedence 55 + for @{ 'CircledE $S }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/cocompose_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/cocompose_2.ma index 252f567bd..d633138cd 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/cocompose_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/cocompose_2.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox( f2 ~∘ break f1 )" right associative with precedence 60 diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/diamond_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/diamond_0.ma index 4f218dd61..8199b1429 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/diamond_0.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/diamond_0.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "◊" non associative with precedence 55 diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/downarrow_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/downarrow_1.ma index e35058c60..46000a861 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/downarrow_1.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/downarrow_1.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox( ↓ term 70 T )" - non associative with precedence 70 - for @{ 'DownArrow $T }. + non associative with precedence 70 + for @{ 'DownArrow $T }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoon_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoon_2.ma index 3b7824afc..646685428 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoon_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoon_2.ma @@ -12,16 +12,16 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation < "hvbox( ⫰ term 46 a )" - non associative with precedence 46 - for @{ 'DownSpoon $S $a }. + non associative with precedence 46 + for @{ 'DownSpoon $S $a }. notation > "hvbox( ⫰ term 46 a )" - non associative with precedence 46 - for @{ 'DownSpoon ? $a }. + non associative with precedence 46 + for @{ 'DownSpoon ? $a }. notation > "hvbox( ⫰{ term 46 S } break term 46 a )" - non associative with precedence 46 - for @{ 'DownSpoon $S $a }. + non associative with precedence 46 + for @{ 'DownSpoon $S $a }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoonstar_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoonstar_3.ma index c6ad562a3..0a57eea4e 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoonstar_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoonstar_3.ma @@ -12,16 +12,16 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation < "hvbox( ⫰*[ break term 46 n ] break term 46 a )" - non associative with precedence 46 - for @{ 'DownSpoonStar $S $n $a }. + non associative with precedence 46 + for @{ 'DownSpoonStar $S $n $a }. notation > "hvbox( ⫰*[ break term 46 n ] break term 46 a )" - non associative with precedence 46 - for @{ 'DownSpoonStar ? $n $a }. + non associative with precedence 46 + for @{ 'DownSpoonStar ? $n $a }. notation > "hvbox( ⫰*{ term 46 S }[ break term 46 n ] break term 46 a )" - non associative with precedence 46 - for @{ 'DownSpoonStar $S $n $a }. + non associative with precedence 46 + for @{ 'DownSpoonStar $S $n $a }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/droppred_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/droppred_1.ma index 7e82080a2..cb0d3c883 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/droppred_1.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/droppred_1.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox( ⫱ term 46 T )" - non associative with precedence 46 - for @{ 'DropPred $T }. + non associative with precedence 46 + for @{ 'DropPred $T }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/droppreds_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/droppreds_2.ma index 90c206208..7336f0cd0 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/droppreds_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/droppreds_2.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox( ⫱ *[ term 46 n ] break term 46 T )" - non associative with precedence 46 - for @{ 'DropPreds $n $T }. + non associative with precedence 46 + for @{ 'DropPreds $n $T }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/exp_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/exp_3.ma index 018bea05a..ea7f39835 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/exp_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/exp_3.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation < "hvbox( f ^ break x )" left associative with precedence 75 diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/identity_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/identity_0.ma index 9d4aea574..97a04ef17 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/identity_0.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/identity_0.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox( 𝐈𝐝 )" - non associative with precedence 90 - for @{ 'Identity }. + non associative with precedence 90 + for @{ 'Identity }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/infinity_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/infinity_0.ma index f5c849158..8a6a2eba9 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/infinity_0.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/infinity_0.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "∞" - non associative with precedence 55 - for @{ 'Infinity }. + non associative with precedence 55 + for @{ 'Infinity }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/no_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/no_0.ma index af692211e..25e0d34cb 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/no_0.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/no_0.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "Ⓕ" non associative with precedence 55 diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/one_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/one_0.ma index 1a6b8474b..ba189fbb9 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/one_0.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/one_0.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "𝟏" non associative with precedence 55 diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/onezero_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/onezero_0.ma index 5df776e6a..640ba879e 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/onezero_0.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/onezero_0.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "𝟙𝟘" - non associative with precedence 55 - for @{ 'OneZero }. + non associative with precedence 55 + for @{ 'OneZero }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/oplusright_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/oplusright_3.ma index e172f4abe..27d9b57ca 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/oplusright_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/oplusright_3.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation < "hvbox( hd ⨮ break tl )" right associative with precedence 47 diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/semicolon_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/semicolon_3.ma index cd884bde6..ee874bc9f 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/semicolon_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/semicolon_3.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox( ❨ term 46 hd1, break term 46 hd2 ❩; break term 46 tl )" non associative with precedence 47 diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/tuple_4.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/tuple_4.ma index 551ee0d94..50b96096d 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/tuple_4.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/tuple_4.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox ( 〈 term 46 x1, break term 46 x2 , break term 46 x3, break term 46 x4 〉 )" non associative with precedence 55 diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/two_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/two_0.ma index 2562f0af7..1f770896c 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/two_0.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/two_0.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "𝟐" non associative with precedence 55 diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/uniform_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/uniform_1.ma index df29e6b1a..ad7877afe 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/uniform_1.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/uniform_1.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox( 𝐔 ❨ break term 46 a ❩ )" non associative with precedence 90 diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/uparrow_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/uparrow_1.ma index 1402237cd..cc3bb324b 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/uparrow_1.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/uparrow_1.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox( ↑ term 70 T )" - non associative with precedence 70 - for @{ 'UpArrow $T }. + non associative with precedence 70 + for @{ 'UpArrow $T }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/uparrowstar_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/uparrowstar_2.ma index 50e07287a..899beb264 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/uparrowstar_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/uparrowstar_2.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox( ↑*[ term 46 n ] break term 70 T )" - non associative with precedence 70 - for @{ 'UpArrowStar $n $T }. + non associative with precedence 70 + for @{ 'UpArrowStar $n $T }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/updownarrowstar_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/updownarrowstar_1.ma index 26ac82e66..47b35d5d9 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/updownarrowstar_1.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/updownarrowstar_1.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox( ↕* term 46 T )" - non associative with precedence 46 - for @{ 'UpDownArrowStar $T }. + non associative with precedence 46 + for @{ 'UpDownArrowStar $T }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/upspoon_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/upspoon_1.ma index 2c71ef371..406f4a866 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/upspoon_1.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/upspoon_1.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox( ⫯ term 46 T )" - non associative with precedence 46 - for @{ 'UpSpoon $T }. + non associative with precedence 46 + for @{ 'UpSpoon $T }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/upspoonstar_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/upspoonstar_2.ma index c9a1e3184..b3b50c643 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/upspoonstar_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/upspoonstar_2.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox( ⫯*[ term 46 n ] break term 46 T )" - non associative with precedence 46 - for @{ 'UpSpoonStar $n $T }. + non associative with precedence 46 + for @{ 'UpSpoonStar $n $T }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/yes_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/yes_0.ma index c321749ae..824475dcc 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/yes_0.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/yes_0.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "Ⓣ" non associative with precedence 55 diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/zero_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/zero_0.ma index 59b76ebb0..50f6bb0db 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/zero_0.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/zero_0.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "𝟎" non associative with precedence 55 diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/zeroone_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/zeroone_0.ma index ff195abe1..a4fabaa47 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/zeroone_0.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/zeroone_0.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "𝟘𝟙" - non associative with precedence 55 - for @{ 'ZeroOne }. + non associative with precedence 55 + for @{ 'ZeroOne }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/zerozero_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/zerozero_0.ma index cb4b10dad..bf415b56a 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/zerozero_0.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/zerozero_0.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "𝟘𝟘" - non associative with precedence 55 - for @{ 'ZeroZero }. + non associative with precedence 55 + for @{ 'ZeroZero }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/doteq_4.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/doteq_4.ma index f3a39a720..ede24a0fe 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/relations/doteq_4.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/doteq_4.ma @@ -12,16 +12,16 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation < "hvbox( f1 ≐ break term 46 f2 )" - non associative with precedence 45 - for @{ 'DotEq $A $B $f1 $f2 }. + non associative with precedence 45 + for @{ 'DotEq $A $B $f1 $f2 }. notation > "hvbox( f1 ≐ break term 46 f2 )" - non associative with precedence 45 - for @{ 'DotEq ? ? $f1 $f2 }. + non associative with precedence 45 + for @{ 'DotEq ? ? $f1 $f2 }. notation > "hvbox( f1 ≐{ break term 46 A, break term 46 B } break term 46 f2 )" - non associative with precedence 45 - for @{ 'DotEq $A $B $f1 $f2 }. + non associative with precedence 45 + for @{ 'DotEq $A $B $f1 $f2 }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/ideq_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/ideq_2.ma index be8260416..8ade3ee43 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/relations/ideq_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/ideq_2.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox( f1 ≡ break term 46 f2 )" - non associative with precedence 45 - for @{ 'IdEq $f1 $f2 }. + non associative with precedence 45 + for @{ 'IdEq $f1 $f2 }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/isdivergent_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/isdivergent_1.ma index 1a25c7878..398b4dfb8 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/relations/isdivergent_1.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/isdivergent_1.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox( 𝛀❪ term 46 f ❫ )" - non associative with precedence 45 - for @{ 'IsDivergent $f }. + non associative with precedence 45 + for @{ 'IsDivergent $f }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/isfinite_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/isfinite_1.ma index ac60a895b..a0bb366a2 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/relations/isfinite_1.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/isfinite_1.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox( 𝐅❪ term 46 f ❫ )" - non associative with precedence 45 - for @{ 'IsFinite $f }. + non associative with precedence 45 + for @{ 'IsFinite $f }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/isidentity_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/isidentity_1.ma index 03fb76098..43fdded1b 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/relations/isidentity_1.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/isidentity_1.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox( 𝐈❪ term 46 f ❫ )" - non associative with precedence 45 - for @{ 'IsIdentity $f }. + non associative with precedence 45 + for @{ 'IsIdentity $f }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/ism_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/ism_2.ma index e40a895ec..687c9e1d3 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/relations/ism_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/ism_2.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox( 𝐌❪ term 46 n, break term 46 c ❫ )" - non associative with precedence 45 - for @{ 'IsM $n $c }. + non associative with precedence 45 + for @{ 'IsM $n $c }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/ist_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/ist_1.ma index 5b4420208..a0801cba7 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/relations/ist_1.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/ist_1.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox( 𝐓❪ term 46 f ❫ )" - non associative with precedence 45 - for @{ 'IsT $f }. + non associative with precedence 45 + for @{ 'IsT $f }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/ist_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/ist_2.ma index e9a96facb..e337f5f29 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/relations/ist_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/ist_2.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox( 𝐓❪ term 46 n, break term 46 c ❫ )" - non associative with precedence 45 - for @{ 'IsT $n $c }. + non associative with precedence 45 + for @{ 'IsT $n $c }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/isuniform_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/isuniform_1.ma index bc66e5c6d..e0f081ca3 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/relations/isuniform_1.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/isuniform_1.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox( 𝐔❪ term 46 f ❫ )" - non associative with precedence 45 - for @{ 'IsUniform $f }. + non associative with precedence 45 + for @{ 'IsUniform $f }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/parallel_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/parallel_2.ma index dbbc88185..66c830c56 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/relations/parallel_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/parallel_2.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox( f1 ∥ break term 46 f2 )" - non associative with precedence 45 - for @{ 'Parallel $f1 $f2 }. + non associative with precedence 45 + for @{ 'Parallel $f1 $f2 }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/rafter_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/rafter_3.ma index c54b60b71..0f4bbd9e9 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/relations/rafter_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/rafter_3.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox( f1 ⊚ break term 46 f2 ≘ break term 46 f )" - non associative with precedence 45 - for @{ 'RAfter $f1 $f2 $f }. + non associative with precedence 45 + for @{ 'RAfter $f1 $f2 $f }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/rat_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/rat_3.ma index 007b7f1a4..63317f836 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/relations/rat_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/rat_3.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox( @❪ term 46 T1 , break term 46 f ❫ ≘ break term 46 T2 )" - non associative with precedence 45 - for @{ 'RAt $T1 $f $T2 }. + non associative with precedence 45 + for @{ 'RAt $T1 $f $T2 }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/rcoafter_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/rcoafter_3.ma index 83fc39664..e3255ea92 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/relations/rcoafter_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/rcoafter_3.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox( f1 ~⊚ break term 46 f2 ≘ break term 46 f )" - non associative with precedence 45 - for @{ 'RCoAfter $f1 $f2 $f }. + non associative with precedence 45 + for @{ 'RCoAfter $f1 $f2 $f }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/rcolength_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/rcolength_2.ma index 785c4cbc5..7a0a82148 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/relations/rcolength_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/rcolength_2.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox( 𝐂❪ term 46 f ❫ ≘ break term 46 n )" - non associative with precedence 45 - for @{ 'RCoLength $f $n }. + non associative with precedence 45 + for @{ 'RCoLength $f $n }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/ringeq_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/ringeq_3.ma index e8ca369b7..1061fc073 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/relations/ringeq_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/ringeq_3.ma @@ -12,16 +12,16 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation < "hvbox( v1 ≗ break term 46 v2 )" - non associative with precedence 45 - for @{ 'RingEq $M $v1 $v2 }. + non associative with precedence 45 + for @{ 'RingEq $M $v1 $v2 }. notation > "hvbox( v1 ≗ break term 46 v2 )" - non associative with precedence 45 - for @{ 'RingEq ? $v1 $v2 }. + non associative with precedence 45 + for @{ 'RingEq ? $v1 $v2 }. notation > "hvbox( v1 ≗{ break term 46 M } break term 46 v2 )" - non associative with precedence 45 - for @{ 'RingEq $M $v1 $v2 }. + non associative with precedence 45 + for @{ 'RingEq $M $v1 $v2 }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/rintersection_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/rintersection_3.ma index e7e93d23c..cd1bd316f 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/relations/rintersection_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/rintersection_3.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox( L1 ⋒ break term 46 L2 ≘ break term 46 L )" - non associative with precedence 45 - for @{ 'RIntersection $L1 $L2 $L }. + non associative with precedence 45 + for @{ 'RIntersection $L1 $L2 $L }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/rminus_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/rminus_3.ma index 87177eb97..683919080 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/relations/rminus_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/rminus_3.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox( T1 ▭ break term 46 T2 ≘ break term 46 T )" - non associative with precedence 45 - for @{ 'RMinus $T1 $T2 $T }. + non associative with precedence 45 + for @{ 'RMinus $T1 $T2 $T }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/runion_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/runion_3.ma index 54b036675..a289dc834 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/relations/runion_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/runion_3.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "hvbox( L1 ⋓ break term 46 L2 ≘ break term 46 L )" - non associative with precedence 45 - for @{ 'RUnion $L1 $L2 $L }. + non associative with precedence 45 + for @{ 'RUnion $L1 $L2 $L }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/and_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/and_2.ma index 854eb7b8c..5184bcd1a 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/and_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/and_2.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation > "hvbox(∧∧ term 34 P0 break & term 34 P1)" - non associative with precedence 35 - for @{ 'and $P0 $P1 }. + non associative with precedence 35 + for @{ 'and $P0 $P1 }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/false_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/false_0.ma index b96432510..56f2cda7a 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/false_0.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/false_0.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "⊥" non associative with precedence 19 diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/or_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/or_2.ma index c5da136f2..b10633313 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/or_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/or_2.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation > "hvbox(∨∨ term 29 P0 break | term 29 P1)" - non associative with precedence 30 - for @{ 'or $P0 $P1 }. + non associative with precedence 30 + for @{ 'or $P0 $P1 }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/true_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/true_0.ma index 7a9ad4366..055bdcf84 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/true_0.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/true_0.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* GROUND NOTATION **********************************************************) notation "⊤" non associative with precedence 19