]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl.ma
update in ground and static_2
[helm.git] / matita / matita / contribs / lambdadelta / ground / lib / stream_hdtl.ma
index 5ddd583d1112a74493c882a3f2506286f38f9428..a23cb4ca8caab2ef31e6eeb7598ead4986d5cf10 100644 (file)
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/notation/functions/downspoon_2.ma".
+include "ground/notation/functions/downdashedarrow_2.ma".
 include "ground/lib/stream.ma".
 
 (* HEAD AND TAIL FOR STREAMS ************************************************)
@@ -27,7 +27,7 @@ defined.
 
 interpretation
   "tail (streams)"
-  'DownSpoon A t = (stream_tl A t).
+  'DownDashedArrow A t = (stream_tl A t).
 
 (* Basic constructions ******************************************************)
 
@@ -36,10 +36,10 @@ lemma stream_hd_cons (A) (a) (t):
 // qed.
 
 lemma stream_tl_cons (A) (a) (t):
-      t = â«°{A}(a⨮t).
+      t = â\87£{A}(a⨮t).
 // qed.
 
 lemma stream_split_tl (A) (t):
-      stream_hd A t â¨® â«°t = t.
+      stream_hd A t â¨® â\87£t = t.
 #A * //
 qed.