Data.CheckedEmpty.List.Quantifiers

Definitions

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

Totality: total
Visibility: public export
Constructors:

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

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

Hints:

Uninhabited (Any p [])

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

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

toExists : Any p xs -> Exists p

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export
Constructors:

Nil : All p []

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

Hint: 

Either (Uninhabited (p x)) (Uninhabited (All p xs)) => Uninhabited (All p (x :: 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 -> Lst ne a

Totality: total
Visibility: public export

all : ((x : a) -> Dec (p x)) -> (xs : Lst {_:6215} 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

HLst : Lst ne Type -> Type

  Heterogeneous list

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

pushIn : (xs : Lst ne a) -> (0 _ : All p xs) -> Lst ne (Subset a p)

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

pushInOutInverse : (xs : Lst ne a) -> (0 prf : All p xs) -> pullOut (pushIn xs prf) = Element xs prf

Totality: total
Visibility: export

pushOutInInverse : (xs : Lst ne (Subset a p)) -> uncurry pushIn (pullOut xs) = xs

Totality: total
Visibility: export