(* *)
(**************************************************************************)
-include "ground/notation/functions/downspoon_2.ma".
+include "ground/notation/functions/downdashedarrow_2.ma".
include "ground/lib/stream.ma".
(* HEAD AND TAIL FOR STREAMS ************************************************)
interpretation
"tail (streams)"
- 'DownSpoon A t = (stream_tl A t).
+ 'DownDashedArrow A t = (stream_tl A t).
(* Basic constructions ******************************************************)
// 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.