IdrisDoc: Data.CoList

Data.CoList

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

The unfoldr builds a list from a seed value. In some cases, unfoldr can undo a foldr operation.

unfoldr (\b => if b == 0 then Nothing else Just (b, b-1)) 10
takeCo : (n : Nat) -> (xs : CoList a) -> List a

Take the first n elements of xs

If there are not enough elements, return the whole coList.

n

how many elements to take

xs

the coList to take them from

data CoList : Type -> Type

Idris will know that it always can produce a new element in finite time

Nil : CoList a
(::) : a -> Delayed Infinite (CoList a) -> CoList a
Fixity
Left associative, precedence 7
(++) : CoList a -> CoList a -> CoList a

Append two CoLists

Fixity
Left associative, precedence 7