(* *)
(**************************************************************************)
-include "ground/notation/functions/downspoon_2.ma".
-include "ground/lib/stream_eq.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 ************************************************)
-definition stream_hd (A:Type[0]): stream A → A ≝
- λt. match t with [ stream_cons a _ ⇒ a ].
+definition stream_hd (A:Type[0]): stream A → A.
+#A * #a #_ @a
+defined.
-definition stream_tl (A:Type[0]): stream A → stream A ≝
- λt. match t with [ stream_cons _ t ⇒ t ].
+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)"
- 'DownSpoon 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 = â\87\82{A}(a⨮t).
// qed.
-lemma eq_stream_split_hd_tl (A) (t):
- stream_hd … t ⨮ ⫰t ≗{A} t.
+lemma stream_split_tl (A) (t):
+ ⇃{A}t ⨮ ⇂t = t.
#A * //
qed.