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)

Hints:

Uninhabited (Any p [])

Uninhabited (p x) => Uninhabited (Any p xs) => Uninhabited (Any p (x :: Delay xs))

toExists : Any p xs -> Exists p

Totality: total
Visibility: public export

toDPair : Any p xs -> DPair a p

Totality: total
Visibility: public export

mapProperty : (p x -> q x) -> Any p l -> Any q l

  Modify the property given a pointwise function

Totality: total
Visibility: export

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

Totality: total
Visibility: public export

pushOut : Functor p => Any (p . q) xs -> p (Any q xs)

Totality: total
Visibility: public export