X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Flib%2Fstream_hdtl.ma;h=d6a9a574243c23fe9e65f2ced8569ce537da3296;hb=8f1a123e61ff079b1f9ad63cc915470ec7e6abf3;hp=a23cb4ca8caab2ef31e6eeb7598ead4986d5cf10;hpb=dc605ae41c39773f55381f241b1ed3db4acf5edd;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl.ma b/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl.ma
index a23cb4ca8..d6a9a5742 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).
+lemma stream_hd_lcons (A) (a) (t):
+      a = ⇃{A}(a⨮t).
 // qed.
 
-lemma stream_tl_cons (A) (a) (t):
-      t = ⇣{A}(a⨮t).
+lemma stream_tl_lcons (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.