(* *)
(**************************************************************************)
-include "ground/notation/functions/downspoon_2.ma".
-include "ground/lib/stream_eq.ma".
-include "ground/lib/arith.ma".
+include "ground/notation/functions/downharpoonleft_2.ma".
+include "ground/notation/functions/downharpoonright_2.ma".
+include "ground/lib/stream.ma".
-(* STREAMS ******************************************************************)
+(* HEAD AND TAIL FOR STREAMS ************************************************)
-definition hd (A:Type[0]): stream A → A ≝
- λt. match t with [ seq a _ ⇒ a ].
+definition stream_hd (A:Type[0]): stream A → A.
+#A * #a #_ @a
+defined.
-definition tl (A:Type[0]): stream A → stream A ≝
- λt. match t with [ seq _ t ⇒ t ].
+interpretation
+ "head (streams)"
+ 'DownHarpoonLeft A t = (stream_hd A t).
-interpretation "tail (stream)" 'DownSpoon A t = (tl A t).
+definition stream_tl (A:Type[0]): stream A → stream A.
+#A * #_ #t @t
+defined.
-(* basic properties *********************************************************)
+interpretation
+ "tail (streams)"
+ 'DownHarpoonRight A t = (stream_tl A t).
-lemma hd_rew (A) (a) (t): a = hd A (a⨮t).
+(* Basic constructions ******************************************************)
+
+lemma stream_hd_cons (A) (a) (t):
+ a = ⇃{A}(a⨮t).
// qed.
-lemma tl_rew (A) (a) (t): t = tl A (a⨮t).
+lemma stream_tl_cons (A) (a) (t):
+ t = ⇂{A}(a⨮t).
// qed.
-lemma eq_stream_split (A) (t): (hd … t) ⨮ ⫰t ≗{A} t.
+lemma stream_split_tl (A) (t):
+ ⇃{A}t ⨮ ⇂t = t.
#A * //
qed.