Idris2Doc : Data.SnocList.Quantifiers

Data.SnocList.Quantifiers

Definitions

dataAny : (0_ : (a->Type)) ->SnocLista->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 : px->Anyp (xs:<x)
  A proof that the rightmost element in the `SnocList` satisfies p
There : Anypxs->Anyp (xs:<x)
  A proof that there is an element the tail of the `SnocList` satisfying p

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

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

Hints:
AllShow (mappxs) =>Show (Allpxs)
Either (Uninhabited (px)) (Uninhabited (Allpxs)) =>Uninhabited (Allp (xs:<x))
length : Allpxs->Nat
Totality: total
Visibility: public export
(++) : Allpxs->Allpys->Allp (xs++ys)
Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7
lengthUnfold : (pxs : Allpxs) ->lengthpxs=lengthxs
Totality: total
Visibility: export
mapProperty : (px->qx) ->Allpl->Allql
  Modify the property given a pointwise function

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

Totality: total
Visibility: public export
all : ((x : a) ->Dec (px)) -> (xs : SnocLista) ->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
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
decide : ((x : a) ->Either (px) (qx)) -> (xs : SnocLista) ->Either (Allpxs) (Anyqxs)
  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