Idris2Doc : Data.List.Quantifiers

# Data.List.Quantifiers

## Definitions

`data Any : (0 _ : (a -> Type)) -> List a -> Type`
`  A proof that some element of a list satisfies some property    @ p the property to be satisfied`

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 `List``
`There : Any p xs -> Any p (x :: xs)`
`  A proof that the satisfying element is in the tail of the `List``

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`
`  Modify the property given a pointwise function`

Totality: total
Visibility: export
`any : ((x : a) -> Dec (p x)) -> (xs : List a) -> Dec (Any p xs)`
`  Given a decision procedure for a property, determine if an element of a  list satisfies it.    @ p the property to be satisfied  @ dec the decision procedure  @ xs the list to examine`

Totality: total
Visibility: public export
`toExists : Any p xs -> Exists p`
`  Forget the membership proof`

Totality: total
Visibility: export
`data All : (0 _ : (a -> Type)) -> List a -> Type`
`  A proof that all elements of a list satisfy a property. It is a list of  proofs, corresponding element-wise to the `List`.`

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))`
`mapProperty : (p x -> q x) -> All p l -> All q l`
`  Modify the property given a pointwise function`

Totality: total
Visibility: export
`imapProperty : (0 i : (a -> Type)) -> (i x => p x -> q x) -> All i as => All p as -> All q as`
`  Modify the property given a pointwise interface function`

Totality: total
Visibility: public export
`forget : All (const type) types -> List type`
`  Forget property source for a homogeneous collection of properties`

Totality: total
Visibility: public export
`all : ((x : a) -> Dec (p x)) -> (xs : List a) -> Dec (All p xs)`
`  Given a decision procedure for a property, decide whether all elements of  a list satisfy it.    @ p the property  @ dec the decision procedure  @ xs the list to examine`

Totality: total
Visibility: public export
`zipPropertyWith : (p x -> q x -> r x) -> All p xs -> All q xs -> All r xs`
Totality: total
Visibility: export
`HList : List Type -> Type`
`  A heterogeneous list of arbitrary types`

Totality: total
Visibility: public export
`splitAt : (xs : List a) -> All p (xs ++ ys) -> (All p xs, All p ys)`
Totality: total
Visibility: export
`take : (xs : List a) -> All p (xs ++ ys) -> All p xs`
Totality: total
Visibility: export
`drop : (xs : List a) -> All p (xs ++ ys) -> All p ys`
Totality: total
Visibility: export
`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 it.`

Totality: total
Visibility: export
`anyNegAll : Any (Not . p) xs -> Not (All p xs)`
`  If there exists an element that doesn't satify the property, then it is  not the case that all elements satisfy it.`

Totality: total
Visibility: export
`allNegAny : All (Not . p) xs -> Not (Any p xs)`
`  If none of the elements satisfy the property, then not any single one can.`

Totality: total
Visibility: export
`indexAll : Elem x xs -> All p xs -> p x`
`  Given a proof of membership for some element, extract the property proof for it`

Totality: total
Visibility: public export
`pushIn : (xs : List a) -> (0 _ : All p xs) -> List (Subset a p)`
`  Push in the property from the list level with element level`

Totality: total
Visibility: public export
`pullOut : List (Subset a p) -> Subset (List a) (All p)`
`  Pull the elementwise property out to the list level`

Totality: total
Visibility: public export
`pushInOutInverse : (xs : List a) -> (0 prf : All p xs) -> pullOut (pushIn xs prf) = Element xs prf`
Totality: total
Visibility: export
`pushOutInInverse : (xs : List (Subset a p)) -> uncurry pushIn (pullOut xs) = xs`
Totality: total
Visibility: export
`data Interleaving : List a -> List a -> List a -> Type`
`  Two lists, `xs` and `ys`, whose elements are interleaved in the list `xys`.`

Totality: total
Visibility: public export
Constructors:
`Nil : Interleaving [] [] []`
`Left : Interleaving xs ys xys -> Interleaving (x :: xs) ys (x :: xys)`
`Right : Interleaving xs ys xys -> Interleaving xs (y :: ys) (y :: xys)`
`record Split : (a -> Type) -> List a -> Type`
`  A record for storing the result of splitting a list `xys` according to some  property `p`.  The `prfs` and `contras` are related to the original list (`xys`) via  `Interleaving`.    @ xys the list which has been split  @ p   the property used for the split`

Totality: total
Visibility: public export
Constructor:
`MkSplit : Interleaving ayes naws xys => All p ayes -> All (Not . p) naws -> Split p xys`

Projections:
`.ayes : Split p xys -> List a`
`.contras : ({rec:0} : Split p xys) -> All (Not . p) (naws {rec:0})`
`  A proof that all elements in `naws` do not satisfy the property used for  the split.`
`.interleaving : ({rec:0} : Split p xys) -> Interleaving (ayes {rec:0}) (naws {rec:0}) xys`
`.naws : Split p xys -> List a`
`.prfs : ({rec:0} : Split p xys) -> All p (ayes {rec:0})`
`  A proof that all elements in `ayes` satisfies the property used for the  split.`
`.naws : Split p xys -> List a`
Totality: total
Visibility: public export
`.ayes : Split p xys -> List a`
Totality: total
Visibility: public export
`naws : Split p xys -> List a`
Totality: total
Visibility: public export
`ayes : Split p xys -> List a`
Totality: total
Visibility: public export
`.interleaving : ({rec:0} : Split p xys) -> Interleaving (ayes {rec:0}) (naws {rec:0}) xys`
Totality: total
Visibility: public export
`interleaving : ({rec:0} : Split p xys) -> Interleaving (ayes {rec:0}) (naws {rec:0}) xys`
Totality: total
Visibility: public export
`.prfs : ({rec:0} : Split p xys) -> All p (ayes {rec:0})`
`  A proof that all elements in `ayes` satisfies the property used for the  split.`

Totality: total
Visibility: public export
`prfs : ({rec:0} : Split p xys) -> All p (ayes {rec:0})`
`  A proof that all elements in `ayes` satisfies the property used for the  split.`

Totality: total
Visibility: public export
`.contras : ({rec:0} : Split p xys) -> All (Not . p) (naws {rec:0})`
`  A proof that all elements in `naws` do not satisfy the property used for  the split.`

Totality: total
Visibility: public export
`contras : ({rec:0} : Split p xys) -> All (Not . p) (naws {rec:0})`
`  A proof that all elements in `naws` do not satisfy the property used for  the split.`

Totality: total
Visibility: public export
`splitOnto : ((x : a) -> Dec (p x)) -> (xs : List a) -> Split p acc -> Split p (reverseOnto acc xs)`
`  Split the list according to the given decidable property, putting the  resulting proofs and contras in an accumulator.    @ dec a function which returns a decidable property  @ xs  a list of elements to split  @ a   the accumulator`

Totality: total
Visibility: public export
`split : ((x : a) -> Dec (p x)) -> (xs : List a) -> Split p (reverse xs)`
`  Split the list according to the given decidable property, starting with an  empty accumulator.  Use `splitOnto` if you want to specify the accumulator.    @ dec a function which returns a decidable property  @ xs  a list of elements to split  @ a   the accumulator`

Totality: total
Visibility: public export
`decide : ((x : a) -> Either (p x) (q x)) -> (xs : List a) -> Either (All p xs) (Any q xs)`
`  If any `a` either satisfies p or q then given a List of as,  either all values satisfy p  or at least one of them sastifies q`

Totality: total
Visibility: public export