From 0ec18c143ce3e5f83b54d5dbe8b1e7275be51da6 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Wed, 3 Sep 2014 13:02:20 +0200 Subject: [PATCH] Repeat function on streams. --- theories/streams.v | 1 + 1 file changed, 1 insertion(+) diff --git a/theories/streams.v b/theories/streams.v index d07e76b6..c39b8ee2 100644 --- a/theories/streams.v +++ b/theories/streams.v @@ -28,6 +28,7 @@ Global Instance stream_fmap : FMap stream := λ A B f, Fixpoint stake {A} (n : nat) (s : stream A) := match n with 0 => [] | S n => shead s :: stake n (stail s) end. +CoFixpoint srepeat {A} (x : A) : stream A := x :.: srepeat x. Section stream_properties. Context {A : Type}. -- GitLab