Data.CheckedEmpty.List.Lazy.Quantifiers

Definitions

data Any : (0 _ : (a -> Type)) -> LazyLst ne a -> Type

Totality: total
Visibility: public export
Constructors:

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

There : Lazy (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))

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

Totality: total
Visibility: public export

any : ((x : a) -> Dec (p x)) -> (xs : LazyLst ne a) -> Dec (Any p xs)

Totality: total
Visibility: export

toExists : Any p xs -> Exists p

Totality: total
Visibility: public export

data All : (0 _ : (a -> Type)) -> LazyLst ne a -> Type

Totality: total
Visibility: public export
Constructors:

Nil : All p []

(::) : p x -> Lazy (All p xs) -> All p (x :: Delay xs)

Hint: 

Either (Uninhabited (p x)) (Uninhabited (All p xs)) => Uninhabited (All p (x :: Delay xs))

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

Totality: total
Visibility: public export

zipPropertyWith : (p x -> q x -> r x) -> All p xs -> All q xs -> All r xs

Totality: total
Visibility: public export

imapProperty : (0 i : (a -> Type)) -> (i x => p x -> q x) -> All i xs => All p xs -> All q xs

Totality: total
Visibility: public export

forget : All (const a) b -> LazyLst ne a

Totality: total
Visibility: public export

all : ((x : a) -> Dec (p x)) -> (xs : LazyLst {_:6221} a) -> Dec (All p xs)

Totality: total
Visibility: public export

index : (idx : Fin (xs .length)) -> All p xs -> p (index idx xs)

Totality: total
Visibility: public export

negAnyAll : Not (Any p xs) -> All (Not . p) xs

Totality: total
Visibility: export

anyNegAll : Any (Not . p) xs -> Not (All p xs)

Totality: total
Visibility: export

allNegAny : All (Not . p) xs -> Not (Any p xs)

Totality: total
Visibility: export

indexAll : Elem x xs -> All p xs -> p x

Totality: total
Visibility: public export

pullOut : LazyLst ne (Subset a p) -> Subset (LazyLst ne a) (All p)

Totality: total
Visibility: public export