Idris2Doc : Data.Vect.Quantifiers

# Data.Vect.Quantifiers

## Definitions

`data Any : (0 _ : (a -> Type)) -> Vect n a -> Type`
`  A proof that some element of a vector satisfies some property    @ p the property to be satsified`

Totality: total
Visibility: public export
Constructors:
`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``

Hints:
`Uninhabited (Any p [])`
`Uninhabited (p x) => Uninhabited (Any p xs) => Uninhabited (Any p (x :: xs))`
`anyElim : (Any p xs -> b) -> (p x -> b) -> Any p (x :: xs) -> b`
`  Eliminator for `Any``

Totality: total
Visibility: public export
`any : ((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`

Totality: total
Visibility: public export
`mapProperty : (p x -> q x) -> Any p l -> Any q l`
Totality: total
Visibility: export
`toExists : Any p xs -> Exists p`
Totality: total
Visibility: export
`anyToFin : Any p xs -> Fin n`
`  Get the bounded numeric position of the element satisfying the predicate`

Totality: total
Visibility: public export
`anyToFinCorrect : (witness : Any p xs) -> p (index (anyToFin witness) xs)`
`  `anyToFin`'s return type satisfies the predicate`

Totality: total
Visibility: export
`data All : (0 _ : (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`.`

Totality: total
Visibility: public export
Constructors:
`Nil : All p []`
`(::) : p x -> All p xs -> All p (x :: xs)`

Hints:
`All (Ord . p) xs => All (Eq . p) xs`
`All (Monoid . p) xs => All (Semigroup . p) xs`
`All (Eq . p) xs => Eq (All p xs)`
`All (Monoid . p) xs => Monoid (All p xs)`
`All (Ord . p) xs => Ord (All p xs)`
`All (Semigroup . p) xs => Semigroup (All p xs)`
`All (Show . p) xs => Show (All p xs)`
`Either (Uninhabited (p x)) (Uninhabited (All p xs)) => Uninhabited (All p (x :: xs))`
`negAnyAll : Not (Any p xs) -> 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
Visibility: export
`notAllHere : Not (p x) -> Not (All p (x :: xs))`
Totality: total
Visibility: export
`notAllThere : Not (All p xs) -> Not (All p (x :: xs))`
Totality: total
Visibility: export
`all : ((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`

Totality: total
Visibility: public export
`mapProperty : (p x -> q x) -> All p l -> All q l`
Totality: total
Visibility: export
`mapPropertyRelevant : ((x : a) -> p x -> q x) -> All p xs -> All q xs`
`  A variant of `mapProperty` that also allows accessing  the values of `xs` that the corresponding `ps` prove `p` about.`

Totality: total
Visibility: export
`imapProperty : (0 i : (a -> Type)) -> (i x => p x -> q x) -> All i as => All p as -> All q as`
Totality: total
Visibility: public export
`forget : All (const p) xs -> Vect n p`
`  If `All` witnesses a property that does not depend on the vector `xs`  it's indexed by, then it is really a `Vect`.`

Totality: total
Visibility: public export
`remember : (xs : Vect n ty) -> All (const ty) xs`
`  Any `Vect` can be lifted to become an `All`  witnessing the presence of elements of the `Vect`'s type.`

Totality: total
Visibility: public export
`forgetRememberId : (xs : Vect n ty) -> forget (remember xs) = xs`
Totality: total
Visibility: export
`castAllConst : All (const ty) xs -> All (const ty) ys`
Totality: total
Visibility: public export
`rememberForgetId : (vs : All (const ty) xs) -> castAllConst (remember (forget vs)) = vs`
Totality: total
Visibility: export
`zipPropertyWith : (p x -> q x -> r x) -> All p xs -> All q xs -> All r xs`
Totality: total
Visibility: export
`traverseProperty : Applicative f => (p x -> f (q x)) -> All p xs -> f (All q xs)`
`  A `Traversable`'s `traverse` for `All`,  for traversals that don't care about the values of the associated `Vect`.`

Totality: total
Visibility: export
`traversePropertyRelevant : Applicative f => ((x : a) -> p x -> f (q x)) -> All p xs -> f (All q xs)`
`  A `Traversable`'s `traverse` for `All`,  in case the elements of the `Vect` that the `All` is proving `p` about are also needed.`

Totality: total
Visibility: export
`tabulate : ((ix : Fin n) -> p (index ix xs)) -> All p xs`
Totality: total
Visibility: public export
`(++) : All p xs -> All p ys -> All p (xs ++ ys)`
Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7
`HVect : Vect n Type -> Type`
`  A heterogeneous vector of arbitrary types`

Totality: total
Visibility: public export
`head : All p (x :: xs) -> p x`
`  Take the first element.`

Totality: total
Visibility: export
`tail : All p (x :: xs) -> All p xs`
`  Take all but the first element.`

Totality: total
Visibility: export
`drop : (n : Nat) -> All p xs -> All p (the (Vect m a) (drop n xs))`
`  Drop the first n elements given knowledge that  there are at least n elements available.`

Totality: total
Visibility: export
`drop' : (l : Nat) -> All p xs -> All p (drop' l xs)`
`  Drop up to the first l elements, stopping early  if all elements have been dropped.`

Totality: total
Visibility: export