WIP: same as Data.List.Quantifiers but for lazy lists
data Any : (a -> Type) -> LazyList a -> Type
Uninhabited (Any p [])
Uninhabited (p x) => Uninhabited (Any p xs) => Uninhabited (Any p (x :: Delay xs))
toExists : Any p xs -> Exists p
toDPair : Any p xs -> DPair a p
mapProperty : (p x -> q x) -> Any p l -> Any q l
Modify the property given a pointwise function
any : ((x : a) -> Dec (p x)) -> (xs : LazyList a) -> Dec (Any p xs)
Given a decision procedure for a property, determine if an element of a
list satisfies it.
@ p the property to be satisfied
@ dec the decision procedure
@ xs the list to examine
pushOut : Functor p => Any (p . q) xs -> p (Any q xs)