Idris2Doc : Data.List1.Quantifiers

Data.List1.Quantifiers

Definitions

dataAny : (0_ : (a->Type)) ->List1a->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 `List1`
There : Anypxs->Anyp (x:::xs)
  A proof that the satisfying element is in the tail of the `List1`
mapProperty : (px->qx) ->Anypl->Anyql
  Modify the property given a pointwise function

Totality: total
Visibility: export
any : ((x : a) ->Dec (px)) -> (xs : List1a) ->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)) ->List1a->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: 
(:::) : px->Allpxs->Allp (x:::xs)

Hint: 
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->List1type
  Forget property source for a homogeneous collection of properties

Totality: total
Visibility: public export
all : ((x : a) ->Dec (px)) -> (xs : List1a) ->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
HList1 : List1Type->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 : List1a) -> (0_ : Allpxs) ->List1 (Subsetap)
  Push in the property from the list level with element level

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

Totality: total
Visibility: public export
pushInOutInverse : (xs : List1a) -> (0prf : Allpxs) ->pullOut (pushInxsprf) =Elementxsprf
Totality: total
Visibility: export
pushOutInInverse : (xs : List1 (Subsetap)) ->uncurrypushIn (pullOutxs) =xs
Totality: total
Visibility: export