From: Ferruccio Guidi Date: Thu, 30 Sep 2021 18:16:10 +0000 (+0200) Subject: update in ground X-Git-Tag: make_still_working~140 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8bbe582d87984526f40182c4409cbfd43108cb79;p=helm.git update in ground + new notation for head and tail --- diff --git a/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl.ma b/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl.ma index a23cb4ca8..468f306de 100644 --- a/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl.ma +++ b/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl.ma @@ -12,7 +12,8 @@ (* *) (**************************************************************************) -include "ground/notation/functions/downdashedarrow_2.ma". +include "ground/notation/functions/downharpoonleft_2.ma". +include "ground/notation/functions/downharpoonright_2.ma". include "ground/lib/stream.ma". (* HEAD AND TAIL FOR STREAMS ************************************************) @@ -21,25 +22,29 @@ definition stream_hd (A:Type[0]): stream A → A. #A * #a #_ @a defined. +interpretation + "head (streams)" + 'DownHarpoonLeft A t = (stream_hd A t). + definition stream_tl (A:Type[0]): stream A → stream A. #A * #_ #t @t defined. interpretation "tail (streams)" - 'DownDashedArrow A t = (stream_tl A t). + 'DownHarpoonRight A t = (stream_tl A t). (* Basic constructions ******************************************************) lemma stream_hd_cons (A) (a) (t): - a = stream_hd A (a⨮t). + a = ⇃{A}(a⨮t). // qed. lemma stream_tl_cons (A) (a) (t): - t = ⇣{A}(a⨮t). + t = ⇂{A}(a⨮t). // qed. lemma stream_split_tl (A) (t): - stream_hd A t ⨮ ⇣t = t. + ⇃{A}t ⨮ ⇂t = t. #A * // qed. diff --git a/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma b/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma index 670790c91..b2f042c1f 100644 --- a/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma +++ b/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground/notation/functions/downdashedarrowstar_3.ma". +include "ground/notation/functions/downharpoonrightstar_3.ma". include "ground/lib/stream_hdtl.ma". include "ground/arith/nat_succ_iter.ma". @@ -23,26 +23,26 @@ definition stream_tls (A) (n): stream A → stream A ≝ interpretation "iterated tail (strams)" - 'DownDashedArrowStar A n f = (stream_tls A n f). + 'DownHarpoonRightStar A n f = (stream_tls A n f). (* Basic constructions ******************************************************) lemma stream_tls_zero (A) (t): - t = ⇣*{A}[𝟎]t. + t = ⇂*{A}[𝟎]t. // qed. lemma stream_tls_tl (A) (n) (t): - (⇣⇣*[n]t) = ⇣*{A}[n]⇣t. + (⇂⇂*[n]t) = ⇂*{A}[n]⇂t. #A #n #t @(niter_appl … (stream_tl …)) qed. lemma stream_tls_succ (A) (n) (t): - (⇣⇣*[n]t) = ⇣*{A}[↑n]t. + (⇂⇂*[n]t) = ⇂*{A}[↑n]t. #A #n #t @(niter_succ … (stream_tl …)) qed. lemma stream_tls_swap (A) (n) (t): - (⇣*[n]⇣t) = ⇣*{A}[↑n]t. + (⇂*[n]⇂t) = ⇂*{A}[↑n]t. // qed. diff --git a/matita/matita/contribs/lambdadelta/ground/lib/stream_tls_eq.ma b/matita/matita/contribs/lambdadelta/ground/lib/stream_tls_eq.ma index de88a638b..28ae10cf0 100644 --- a/matita/matita/contribs/lambdadelta/ground/lib/stream_tls_eq.ma +++ b/matita/matita/contribs/lambdadelta/ground/lib/stream_tls_eq.ma @@ -20,7 +20,7 @@ include "ground/lib/stream_tls.ma". (* Constructions with stream_eq *********************************************) lemma stream_tls_eq_repl (A) (n): - stream_eq_repl A (λt1,t2. ⇣*[n] t1 ≗ ⇣*[n] t2). + stream_eq_repl A (λt1,t2. ⇂*[n] t1 ≗ ⇂*[n] t2). #A #n @(nat_ind_succ … n) -n // #n #IH * #n1 #t1 * #n2 #t2 #H elim (stream_eq_inv_cons_bi … H) /2 width=7 by/ diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/downdashedarrow_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/downdashedarrow_2.ma deleted file mode 100644 index 4614cf3a3..000000000 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/downdashedarrow_2.ma +++ /dev/null @@ -1,27 +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 *) -(* *) -(**************************************************************************) - -(* GROUND NOTATION **********************************************************) - -notation < "hvbox( ⇣ term 75 a )" - non associative with precedence 75 - for @{ 'DownDashedArrow $S $a }. - -notation > "hvbox( ⇣ term 75 a )" - non associative with precedence 75 - for @{ 'DownDashedArrow ? $a }. - -notation > "hvbox( ⇣{ term 46 S } break term 75 a )" - non associative with precedence 75 - for @{ 'DownDashedArrow $S $a }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/downdashedarrowstar_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/downdashedarrowstar_3.ma deleted file mode 100644 index 919695181..000000000 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/downdashedarrowstar_3.ma +++ /dev/null @@ -1,27 +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 *) -(* *) -(**************************************************************************) - -(* GROUND NOTATION **********************************************************) - -notation < "hvbox( ⇣*[ break term 46 n ] break term 75 a )" - non associative with precedence 75 - for @{ 'DownDashedArrowStar $S $n $a }. - -notation > "hvbox( ⇣*[ break term 46 n ] break term 75 a )" - non associative with precedence 75 - for @{ 'DownDashedArrowStar ? $n $a }. - -notation > "hvbox( ⇣*{ term 46 S }[ break term 46 n ] break term 75 a )" - non associative with precedence 75 - for @{ 'DownDashedArrowStar $S $n $a }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/downharpoonleft_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/downharpoonleft_2.ma new file mode 100644 index 000000000..ca6946fb3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/downharpoonleft_2.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 *) +(* *) +(**************************************************************************) + +(* GROUND NOTATION **********************************************************) + +notation < "hvbox( ⇃ term 75 a )" + non associative with precedence 75 + for @{ 'DownHarpoonLeft $S $a }. + +notation > "hvbox( ⇃ term 75 a )" + non associative with precedence 75 + for @{ 'DownHarpoonLeft ? $a }. + +notation > "hvbox( ⇃{ term 46 S } break term 75 a )" + non associative with precedence 75 + for @{ 'DownHarpoonLeft $S $a }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/downharpoonright_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/downharpoonright_2.ma new file mode 100644 index 000000000..3fdc1a8dc --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/downharpoonright_2.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 *) +(* *) +(**************************************************************************) + +(* GROUND NOTATION **********************************************************) + +notation < "hvbox( ⇂ term 75 a )" + non associative with precedence 75 + for @{ 'DownHarpoonRight $S $a }. + +notation > "hvbox( ⇂ term 75 a )" + non associative with precedence 75 + for @{ 'DownHarpoonRight ? $a }. + +notation > "hvbox( ⇂{ term 46 S } break term 75 a )" + non associative with precedence 75 + for @{ 'DownHarpoonRight $S $a }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/downharpoonrightstar_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/downharpoonrightstar_3.ma new file mode 100644 index 000000000..017bd72d6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/downharpoonrightstar_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 *) +(* *) +(**************************************************************************) + +(* GROUND NOTATION **********************************************************) + +notation < "hvbox( ⇂*[ break term 46 n ] break term 75 a )" + non associative with precedence 75 + for @{ 'DownHarpoonRightStar $S $n $a }. + +notation > "hvbox( ⇂*[ break term 46 n ] break term 75 a )" + non associative with precedence 75 + for @{ 'DownHarpoonRightStar ? $n $a }. + +notation > "hvbox( ⇂*{ term 46 S }[ break term 46 n ] break term 75 a )" + non associative with precedence 75 + for @{ 'DownHarpoonRightStar $S $n $a }. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tl.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tl.ma index 909430cd9..2d395b69b 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tl.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tl.ma @@ -19,7 +19,7 @@ include "ground/relocation/gr_map.ma". (* TAIL FOR GENERIC RELOCATION MAPS *****************************************) (*** tl *) -definition gr_tl (f): gr_map ≝ ⇣f. +definition gr_tl (f): gr_map ≝ ⇂f. interpretation "tail (generic relocation maps)" diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls.ma index d15047b0c..6b52f7971 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls.ma @@ -19,7 +19,7 @@ include "ground/relocation/gr_tl.ma". (* ITERATED TAIL FOR GENERIC RELOCATION MAPS ********************************) (*** tls *) -definition gr_tls (n) (f:gr_map) ≝ ⇣*[n]f. +definition gr_tls (n) (f:gr_map) ≝ ⇂*[n]f. interpretation "iterated tail (generic relocation maps)" diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl index ece01e73c..d710f3add 100644 --- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl +++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl @@ -118,8 +118,8 @@ table { class "yellow" [ { "extensions to the library" * } { [ { "streams" * } { - [ "stream_tls ( ⇣*{?}[?]? )" "stream_tls_eq" * ] - [ "stream_hdtl ( ⇣{?}? )" * ] + [ "stream_tls ( ⇂*{?}[?]? )" "stream_tls_eq" * ] + [ "stream_hdtl ( ⇃{?}? ) ( ⇂{?}? )" * ] [ "stream_eq ( ? ≗{?} ? )" "stream_eq_eq" * ] [ "stream ( ? ⨮{?} ? )" * ] } diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index 671b2b031..67c3571a4 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1521,7 +1521,7 @@ let predefined_classes = [ ["⇕"; "⇳"; "⬍"; "↕"; ]; ["↔"; "⇔"; "⬄"; "⬌"; ] ; ["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; "⊆"; "⫃"; "⊑"; ] ; - ["_"; "↓"; "↙"; "⇣"; "⎽"; "⎼"; "⎻"; "⎺"; ]; + ["_"; "↓"; "↙"; "⇣"; "⇃"; "⇂"; "⎽"; "⎼"; "⎻"; "⎺"; ]; ["<"; "≺"; "≮"; "⊀"; "〈"; "«"; "❬"; "❮"; "❰"; ] ; ["("; "❨"; "❪"; "❲"; "（"; ]; [")"; "❩"; "❫"; "❳"; "）"; ];