Add forgotten module
commit9a1b66feee1e6a6a8b2e1f1a09bccd747954de17
authorDavid Christiansen <david@davidchristiansen.dk>
dateTue 19 Nov 2013, 18:55 (13 years ago)
parent4ec6896
lib/Prelude/Stream.idrnew file+10
@@ -0,0 +1,10 @@
1+module Prelude.Stream
2+
3+import Prelude.Vect
4+
5+codata Stream : Type -> Type where
6+ (::) : a -> Stream a -> Stream a
7+
8+take : (n : Nat) -> Stream a -> Vect n a
9+take Z _ = []
10+take (S n) (x :: xs) = x :: (take n xs)