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 a23cb4ca8caab2ef31e6eeb7598ead4986d5cf10..468f306de0bbcbd4429b6a4607b69779e0a31e8e 100644 (file)
--- 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 = â\87£{A}(a⨮t).
+      t = â\87\82{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 670790c914e74ca46928b2500303a39c37b1fe6f..b2f042c1f20faeae78cba32d601ea94e3952b311 100644 (file)
--- 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 = â\87£*{A}[𝟎]t.
+      t = â\87\82*{A}[𝟎]t.
 // qed.
 
 lemma stream_tls_tl (A) (n) (t):
-      (â\87£â\87£*[n]t) = â\87£*{A}[n]â\87£t.
+      (â\87\82â\87\82*[n]t) = â\87\82*{A}[n]â\87\82t.
 #A #n #t
 @(niter_appl … (stream_tl …))
 qed.
 
 lemma stream_tls_succ (A) (n) (t):
-      (â\87£â\87£*[n]t) = â\87£*{A}[↑n]t.
+      (â\87\82â\87\82*[n]t) = â\87\82*{A}[↑n]t.
 #A #n #t
 @(niter_succ … (stream_tl …))
 qed.
 
 lemma stream_tls_swap (A) (n) (t):
-      (â\87£*[n]â\87£t) = â\87£*{A}[↑n]t.
+      (â\87\82*[n]â\87\82t) = â\87\82*{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 de88a638b1d4889a4d3721a94e5d9db456937193..28ae10cf0859075a124b2ae558dbb5665e2a4a81 100644 (file)
--- 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. â\87£*[n] t1 â\89\97 â\87£*[n] t2).
+      stream_eq_repl A (λt1,t2. â\87\82*[n] t1 â\89\97 â\87\82*[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 (file)
index 4614cf3..0000000
--- 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 (file)
index 9196951..0000000
--- 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 (file)
index 0000000..ca6946f
--- /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 (file)
index 0000000..3fdc1a8
--- /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 (file)
index 0000000..017bd72
--- /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 909430cd9648cab66cb9702f9fadd922aed5aa5f..2d395b69ba28fbf6adf196cdf0a6bd4ae63ddb0b 100644 (file)
--- 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 â\89\9d â\87£f.
+definition gr_tl (f): gr_map â\89\9d â\87\82f.
 
 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 d15047b0c63783a7bd033af33eff400b9a832998..6b52f797142e07007f2f7864fe3cf1714d1066b3 100644 (file)
--- 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) â\89\9d â\87£*[n]f.
+definition gr_tls (n) (f:gr_map) â\89\9d â\87\82*[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 ece01e73c0a1703d561faf0499892e282a122f36..d710f3addfc4e14d645fb88ffbbb5abbb06597ba 100644 (file)
--- 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 ( â\87£*{?}[?]? )" "stream_tls_eq" * ]
-          [ "stream_hdtl ( â\87£{?}? )" * ]
+          [ "stream_tls ( â\87\82*{?}[?]? )" "stream_tls_eq" * ]
+          [ "stream_hdtl ( â\87\83{?}? ) ( â\87\82{?}? )" * ]
           [ "stream_eq ( ? ≗{?} ? )" "stream_eq_eq" * ]
           [ "stream ( ? ⨮{?} ? )" * ]
         }

diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index 671b2b0319bf48bc296b858df925987381ca8b82..67c3571a48f954de4bd368b4c8b559d542c2ceb7 100644 (file)
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1521,7 +1521,7 @@ let predefined_classes = [
  ["⇕"; "⇳"; "⬍"; "↕"; ];
  ["↔"; "⇔"; "⬄"; "⬌"; ] ; 
  ["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; "⊆"; "⫃"; "⊑"; ] ;
- ["_"; "↓"; "↙"; "⇣"; "⎽"; "⎼"; "⎻"; "⎺"; ];
+ ["_"; "â\86\93"; "â\86\99"; "â\87£"; "â\87\83"; "â\87\82"; "â\8e½"; "â\8e¼"; "â\8e»"; "â\8eº"; ];
  ["<"; "≺"; "≮"; "⊀"; "〈"; "«"; "❬"; "❮"; "❰"; ] ;
  ["("; "❨"; "❪"; "❲"; "（"; ];
  [")"; "❩"; "❫"; "❳"; "）"; ];