From 2dc8dc840f40969804f478a1a72cf5ef3b0ef530 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 4 Jul 2014 17:09:57 +0200
Subject: [PATCH] Misc functions on streams.

---
 theories/streams.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/theories/streams.v b/theories/streams.v
index 4b4622a7..d07e76b6 100644
--- a/theories/streams.v
+++ b/theories/streams.v
@@ -23,6 +23,12 @@ Fixpoint slookup {A} (i : nat) (s : stream A) : A :=
   match i with O => shead s | S i => stail s !.! i end
 where "s !.! i" := (slookup i s).
 
+Global Instance stream_fmap : FMap stream := λ A B f,
+  cofix go s := f (shead s) :.: go (stail s).
+
+Fixpoint stake {A} (n : nat) (s : stream A) :=
+  match n with 0 => [] | S n => shead s :: stake n (stail s) end.
+
 Section stream_properties.
 Context {A : Type}.
 Implicit Types x y : A.
-- 
GitLab