Idris2Doc : Data.Vect.Quantifiers

Data.Vect.Quantifiers

All : (0 _ : (a -> Type)) -> Vectna -> Type
A proof that all elements of a vector satisfy a property. It is a list of
proofs, corresponding element-wise to the `Vect`.
Totality: total
Constructors:
Nil : AllpNil
(::) : px -> Allpxs -> Allp (x::xs)
Any : (0 _ : (a -> Type)) -> Vectna -> Type
A proof that some element of a vector satisfies some property

@ p the property to be satsified
Totality: total
Constructors:
Here : px -> Anyp (x::xs)
A proof that the satisfying element is the first one in the `Vect`
There : Anypxs -> Anyp (x::xs)
A proof that the satsifying element is in the tail of the `Vect`
all : ((x : a) -> Dec (px)) -> (xs : Vectna) -> Dec (Allpxs)
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
any : ((x : a) -> Dec (px)) -> (xs : Vectna) -> Dec (Anypxs)
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
anyElim : (Anypxs -> b) -> (px -> b) -> Anyp (x::xs) -> b
Eliminator for `Any`
negAnyAll : Not (Anypxs) -> All (Not.p) xs
If there does not exist an element that satifies the property, then it is
the case that all elements do not satisfy.
notAllHere : Not (px) -> Allp (x::xs) -> Void
notAllThere : Not (Allpxs) -> Allp (x::xs) -> Void