Data.List.Lazy.Quantifiers

WIP: same as Data.List.Quantifiers but for lazy lists

Definitions

data Any : (a -> Type) -> LazyList a -> Type

Totality: total
Visibility: public export
Constructors:

Here : p x -> Any p (x :: xs)

There : Any p (Force xs) -> Any p (x :: xs)

toExists : Any p xs -> Exists p

Totality: total
Visibility: public export

toDPair : Any p xs -> DPair a p

Totality: total
Visibility: public export