Commit 0ec18c14 authored by Robbert Krebbers's avatar Robbert Krebbers

Repeat function on streams.

parent 2e1b8a41
...@@ -28,6 +28,7 @@ Global Instance stream_fmap : FMap stream := λ A B f, ...@@ -28,6 +28,7 @@ Global Instance stream_fmap : FMap stream := λ A B f,
Fixpoint stake {A} (n : nat) (s : stream A) := Fixpoint stake {A} (n : nat) (s : stream A) :=
match n with 0 => [] | S n => shead s :: stake n (stail s) end. 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. Section stream_properties.
Context {A : Type}. Context {A : Type}.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment