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:
  
All (Eq . p) xs => Eq (Any p xs)
  
All (Show . p) xs => Show (Any p xs)
  
All (Uninhabited . p) xs => Uninhabited (Any p xs)
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 (Any 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 (Any p xs)
  
All (Show . p) xs => Show (All p xs)
  
All (Uninhabited . p) xs => Uninhabited (Any p xs)
  
Either (Uninhabited (p x)) (Uninhabited (All p xs)) => Uninhabited (All 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
toDPair : Any p xs -> DPair a p
  Forget the membership proof

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

  Totality: total
  Visibility: export
anyToFin : Any p xs -> Fin (length xs)
  Totality: total
  Visibility: public export
anyToFinCorrect : (witness : Any p xs) -> p (index' xs (anyToFin witness))
  Totality: total
  Visibility: export
anyToFinV : Any p xs -> (idx : Fin (length xs) ** p (index' xs idx))
  Totality: total
  Visibility: public export
pushOut : Functor p => Any (p . q) xs -> p (Any q xs)
  Totality: total
  Visibility: public export
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
(++) : All p xs -> All p ys -> All p (xs ++ ys)
  Concatenate lists of proofs.

  Totality: total
  Visibility: public export
  Fixity Declaration: infixr operator, level 7
head : All p (x :: xs) -> p x
  Take the first element.

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

  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
drop' : (l : Nat) -> All p xs -> All p (drop l xs)
  Totality: total
  Visibility: 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
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
index : (idx : Fin (length xs)) -> All p xs -> p (index' xs idx)
  Given an index of an element, extract the property proof for it

  Totality: total
  Visibility: public export
pushOut : Applicative p => All (p . q) xs -> p (All q xs)
  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
allAnies : All p xs -> List (Any p xs)
  Totality: total
  Visibility: public export
altAll : Alternative p => All (p . q) xs -> p (Any q 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