Idris2Doc : Data.Vect.Quantifiers

# Data.Vect.Quantifiers

dataAll : (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 : Allp []
(::) : px -> Allpxs -> Allp (x::xs)
dataAny : (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`

Totality: total
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`

Totality: total
anyElim : (Anypxs -> b) -> (px -> b) -> Anyp (x::xs) -> b
`  Eliminator for `Any``

Totality: total
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.`

Totality: total
notAllHere : Not (px) -> Not (Allp (x::xs))
Totality: total
notAllThere : Not (Allpxs) -> Not (Allp (x::xs))
Totality: total