Idris2Doc : Data.List.Quantifiers

Data.List.Quantifiers

Definitions

dataAny : (0_ : (a->Type)) ->Lista->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 : px->Anyp (x::xs)
  A proof that the satisfying element is the first one in the `List`
There : Anypxs->Anyp (x::xs)
  A proof that the satisfying element is in the tail of the `List`

Hints:
Uninhabited (Anyp [])
Uninhabited (px) =>Uninhabited (Anypxs) =>Uninhabited (Anyp (x::xs))
mapProperty : (px->qx) ->Anypl->Anyql
  Modify the property given a pointwise function

Totality: total
Visibility: export
any : ((x : a) ->Dec (px)) -> (xs : Lista) ->Dec (Anypxs)
  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 : Anypxs->Existsp
  Forget the membership proof

Totality: total
Visibility: export
dataAll : (0_ : (a->Type)) ->Lista->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 : Allp []
(::) : px->Allpxs->Allp (x::xs)

Hints:
AllShow (mappxs) =>Show (Allpxs)
Either (Uninhabited (px)) (Uninhabited (Allpxs)) =>Uninhabited (Allp (x::xs))
mapProperty : (px->qx) ->Allpl->Allql
  Modify the property given a pointwise function

Totality: total
Visibility: export
imapProperty : (0i : (Type->Type)) -> (ia=>pa->qa) ->Allitypes=>Allptypes->Allqtypes
  Modify the property given a pointwise interface function

Totality: total
Visibility: public export
forget : All (consttype) types->Listtype
  Forget property source for a homogeneous collection of properties

Totality: total
Visibility: public export
all : ((x : a) ->Dec (px)) -> (xs : Lista) ->Dec (Allpxs)
  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 : (px->qx->rx) ->Allpxs->Allqxs->Allrxs
Totality: total
Visibility: export
HList : ListType->Type
  A heterogeneous list of arbitrary types

Totality: total
Visibility: public export
negAnyAll : Not (Anypxs) ->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 (Allpxs)
  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 (Anypxs)
  If none of the elements satisfy the property, then not any single one can.

Totality: total
Visibility: export
indexAll : Elemxxs->Allpxs->px
  Given a proof of membership for some element, extract the property proof for it

Totality: total
Visibility: public export
pushIn : (xs : Lista) -> (0_ : Allpxs) ->List (Subsetap)
  Push in the property from the list level with element level

Totality: total
Visibility: public export
pullOut : List (Subsetap) ->Subset (Lista) (Allp)
  Pull the elementwise property out to the list level

Totality: total
Visibility: public export
pushInOutInverse : (xs : Lista) -> (0prf : Allpxs) ->pullOut (pushInxsprf) =Elementxsprf
Totality: total
Visibility: export
pushOutInInverse : (xs : List (Subsetap)) ->uncurrypushIn (pullOutxs) =xs
Totality: total
Visibility: export
dataInterleaving : Lista->Lista->Lista->Type
  Two lists, `xs` and `ys`, whose elements are interleaved in the list `xys`.

Totality: total
Visibility: public export
Constructors:
Nil : Interleaving [] [] []
Left : Interleavingxsysxys->Interleaving (x::xs) ys (x::xys)
Right : Interleavingxsysxys->Interleavingxs (y::ys) (y::xys)
recordSplit : (a->Type) ->Lista->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 : Interleavingayesnawsxys=>Allpayes->All (Not.p) naws->Splitpxys

Projections:
.ayes : Splitpxys->Lista
.contras : ({rec:0} : Splitpxys) ->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} : Splitpxys) ->Interleaving (ayes{rec:0}) (naws{rec:0}) xys
.naws : Splitpxys->Lista
.prfs : ({rec:0} : Splitpxys) ->Allp (ayes{rec:0})
  A proof that all elements in `ayes` satisfies the property used for the
split.
.naws : Splitpxys->Lista
Totality: total
Visibility: public export
.ayes : Splitpxys->Lista
Totality: total
Visibility: public export
naws : Splitpxys->Lista
Totality: total
Visibility: public export
ayes : Splitpxys->Lista
Totality: total
Visibility: public export
.interleaving : ({rec:0} : Splitpxys) ->Interleaving (ayes{rec:0}) (naws{rec:0}) xys
Totality: total
Visibility: public export
interleaving : ({rec:0} : Splitpxys) ->Interleaving (ayes{rec:0}) (naws{rec:0}) xys
Totality: total
Visibility: public export
.prfs : ({rec:0} : Splitpxys) ->Allp (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} : Splitpxys) ->Allp (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} : Splitpxys) ->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} : Splitpxys) ->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 (px)) -> (xs : Lista) ->Splitpacc->Splitp (reverseOntoaccxs)
  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 (px)) -> (xs : Lista) ->Splitp (reversexs)
  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 (px) (qx)) -> (xs : Lista) ->Either (Allpxs) (Anyqxs)
  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