Idris2Doc : Data.SnocList.Quantifiers

# Data.SnocList.Quantifiers

## Definitions

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

Totality: total
Visibility: public export
Constructors:
`Here : p x -> Any p (xs :< x)`
`  A proof that the rightmost element in the `SnocList` satisfies p`
`There : Any p xs -> Any p (xs :< x)`
`  A proof that there is an element the tail of the `SnocList` satisfying p`

Hints:
`Uninhabited (Any p [<])`
`Uninhabited (p x) => Uninhabited (Any p xs) => Uninhabited (Any p (xs :< x))`
`mapProperty : (p x -> q x) -> Any p l -> Any q l`
`  Modify the property given a pointwise function`

Totality: total
Visibility: public export
`any : ((x : a) -> Dec (p x)) -> (xs : SnocList 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)) -> SnocList 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:
`Lin : All p [<]`
`(:<) : All p xs -> p x -> All p (xs :< x)`

Hints:
`All Show (map p xs) => Show (All p xs)`
`Either (Uninhabited (p x)) (Uninhabited (All p xs)) => Uninhabited (All p (xs :< x))`
`length : All p xs -> Nat`
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
`lengthUnfold : (pxs : All p xs) -> length pxs = length xs`
Totality: total
Visibility: export
`mapProperty : (p x -> q x) -> All p l -> All q l`
`  Modify the property given a pointwise function`

Totality: total
Visibility: public 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 -> SnocList type`
`  Forget property source for a homogeneous collection of properties`

Totality: total
Visibility: public export
`all : ((x : a) -> Dec (p x)) -> (xs : SnocList 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
`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
`decide : ((x : a) -> Either (p x) (q x)) -> (xs : SnocList a) -> Either (All p xs) (Any q xs)`
`  If any `a` either satisfies p or q then given a Snoclist of as,  either all values satisfy p  or at least one of them sastifies q`

Totality: total
Visibility: public export