Data.List.Lazy

Definitions

data LazyList : Type -> Type

Totality: total
Visibility: public export
Constructors:

Nil : LazyList a

(::) : a -> Lazy (LazyList a) -> LazyList a

Hints:

Alternative LazyList

Applicative LazyList

Eq a => Eq (LazyList a)

Foldable LazyList

Functor LazyList

Monad LazyList

Monoid (LazyList a)

Ord a => Ord (LazyList a)

Semigroup (LazyList a)

Show a => Show (LazyList a)

Zippable LazyList

foldrLazy : (a -> Lazy acc -> acc) -> Lazy acc -> LazyList a -> acc

Totality: total
Visibility: public export

(++) : LazyList a -> Lazy (LazyList a) -> LazyList a

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7

bindLazy : (a -> LazyList b) -> LazyList a -> LazyList b

Totality: total
Visibility: public export

choice : Alternative f => LazyList (f a) -> f a

Totality: total
Visibility: public export

choiceMap : Alternative f => (a -> f b) -> LazyList a -> f b

Totality: total
Visibility: public export

any : (a -> Bool) -> LazyList a -> Bool

Totality: total
Visibility: public export

all : (a -> Bool) -> LazyList a -> Bool

Totality: total
Visibility: public export

traverse : Monad f => (a -> f b) -> LazyList a -> f (List b)

Totality: total
Visibility: public export

for : Monad f => LazyList a -> (a -> f b) -> f (List b)

Totality: total
Visibility: public export

sequence : Monad f => LazyList (f a) -> f (List a)

Totality: total
Visibility: public export

traverse_ : Monad m => (a -> m b) -> LazyList a -> m ()

Totality: total
Visibility: public export

for_ : Monad m => LazyList a -> (a -> m b) -> m ()

Totality: total
Visibility: public export

sequence_ : Monad m => LazyList (m a) -> m ()

Totality: total
Visibility: public export

fromList : List a -> LazyList a

Totality: total
Visibility: public export

iterate : (a -> Maybe a) -> a -> LazyList a

Visibility: public export

unfoldr : (b -> Maybe (a, b)) -> b -> LazyList a

Visibility: public export

iterateN : Nat -> (a -> a) -> a -> LazyList a

Totality: total
Visibility: public export

replicate : Nat -> a -> LazyList a

Totality: total
Visibility: public export

head' : LazyList a -> Maybe a

Totality: total
Visibility: public export

tail' : LazyList a -> Maybe (LazyList a)

Totality: total
Visibility: public export

take : Nat -> LazyList a -> LazyList a

Totality: total
Visibility: public export

drop : Nat -> LazyList a -> LazyList a

Totality: total
Visibility: public export

takeWhile : (a -> Bool) -> LazyList a -> LazyList a

Totality: total
Visibility: public export

dropWhile : (a -> Bool) -> LazyList a -> LazyList a

Totality: total
Visibility: public export

filter : (a -> Bool) -> LazyList a -> LazyList a

Totality: total
Visibility: public export

mapMaybe : (a -> Maybe b) -> LazyList a -> LazyList b

Totality: total
Visibility: public export

take : Fuel -> Stream a -> LazyList a

Totality: total
Visibility: public export

take : Fuel -> Colist a -> LazyList a

Totality: total
Visibility: public export

take : Fuel -> Colist1 a -> LazyList a

Totality: total
Visibility: public export

mergeReplicate : a -> LazyList a -> LazyList a

Totality: total
Visibility: public export

intersperse : a -> LazyList a -> LazyList a

Totality: total
Visibility: public export

intercalate : LazyList a -> LazyList (LazyList a) -> LazyList a

Totality: total
Visibility: public export

toColist : LazyList a -> Colist a

Totality: total
Visibility: public export