Idris2Doc : Data.List1.Quantifiers

# Data.List1.Quantifiers

## Definitions

`data Any : (0 _ : (a -> Type)) -> List1 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 `List1``
`There : Any p xs -> Any p (x ::: xs)`
`  A proof that the satisfying element is in the tail of the `List1``
`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 : List1 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)) -> List1 a -> Type`
`  A proof that all elements of a list satisfy a property. It is a list of  proofs, corresponding element-wise to the `List1`.`

Totality: total
Visibility: public export
Constructor:
`(:::) : p x -> All p xs -> All p (x ::: xs)`

Hint:
`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 : (Type -> Type)) -> (i a => p a -> q a) -> All i types => All p types -> All q types`
`  Modify the property given a pointwise interface function`

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

Totality: total
Visibility: public export
`all : ((x : a) -> Dec (p x)) -> (xs : List1 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
`HList1 : List1 Type -> Type`
`  A heterogeneous list of arbitrary types`

Totality: total
Visibility: public 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 : List1 a) -> (0 _ : All p xs) -> List1 (Subset a p)`
`  Push in the property from the list level with element level`

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

Totality: total
Visibility: public export
`pushInOutInverse : (xs : List1 a) -> (0 prf : All p xs) -> pullOut (pushIn xs prf) = Element xs prf`
Totality: total
Visibility: export
`pushOutInInverse : (xs : List1 (Subset a p)) -> uncurry pushIn (pullOut xs) = xs`
Totality: total
Visibility: export