IdrisDoc: Data.Vect.Quantifiers

Data.Vect.Quantifiers

notAllThere : Not (All P xs) -> All P (x :: xs) -> Void
notAllHere : Not (P x) -> All P (x :: xs) -> Void
negAnyAll : Not (Any P xs) -> All (\x => Not (P x)) xs

If there does not exist an element that satifies the property, then it is
the case that all elements do not satisfy.

anyNilAbsurd : Any P [] -> Void

No element of an empty vector satisfies any property

anyElim : (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b

Eliminator for Any

any : (dec : (x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (Any P xs)

Given a decision procedure for a property, determine if an element of a
vector satisfies it.

P

the property to be satisfied

dec

the decision procedure

xs

the vector to examine

all : (dec : (x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (All P xs)

Given a decision procedure for a property, decide whether all elements of
a vector satisfy it.

P

the property

dec

the decision procedure

xs

the vector to examine

data Any : (P : a -> Type) -> Vect n a -> Type

A proof that some element of a vector satisfies some property

P

the property to be satsified

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

A proof that the satisfying element is the first one in the Vect

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

A proof that the satsifying element is in the tail of the Vect

data All : (P : a -> Type) -> Vect n a -> Type

A proof that all elements of a vector satisfy a property. It is a list of
proofs, corresponding element-wise to the Vect.

Nil : All P []
(::) : P x -> All P xs -> All P (x :: xs)
Fixity
Left associative, precedence 7