Idris2Doc : Data.List.Lazy.Quantifiers

Data.List.Lazy.Quantifiers(source)

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

Definitions

dataAny : (a->Type) ->LazyLista->Type
Totality: total
Visibility: public export
Constructors:
Here : px->Anyp (x::xs)
There : Anyp (Force xs) ->Anyp (x::xs)

Hints:
Uninhabited (Anyp [])
Uninhabited (px) =>Uninhabited (Anypxs) =>Uninhabited (Anyp (x:: Delay xs))
toExists : Anypxs->Existsp
Totality: total
Visibility: public export
toDPair : Anypxs->DPairap
Totality: total
Visibility: public export
mapProperty : (px->qx) ->Anypl->Anyql
  Modify the property given a pointwise function

Totality: total
Visibility: export
any : ((x : a) ->Dec (px)) -> (xs : LazyLista) ->Dec (Anypxs)
  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 : Functorp=>Any (p.q) xs->p (Anyqxs)
Totality: total
Visibility: public export