Idris2Doc : Data.Vect.Quantifiers

Data.Vect.Quantifiers

Definitions

dataAny : (0_ : (a->Type)) ->Vectna->Type
  A proof that some element of a vector satisfies some property

@ p the property to be satsified

Totality: total
Visibility: public export
Constructors:
Here : px->Anyp (x::xs)
  A proof that the satisfying element is the first one in the `Vect`
There : Anypxs->Anyp (x::xs)
  A proof that the satsifying element is in the tail of the `Vect`

Hints:
Uninhabited (Anyp [])
Uninhabited (px) =>Uninhabited (Anypxs) =>Uninhabited (Anyp (x::xs))
anyElim : (Anypxs->b) -> (px->b) ->Anyp (x::xs) ->b
  Eliminator for `Any`

Totality: total
Visibility: public export
any : ((x : a) ->Dec (px)) -> (xs : Vectna) ->Dec (Anypxs)
  Given a decision procedure for a property, determine if an element of a
vector satisfies it.

@ p the property to be satisfied
@ dec the decision procedure
@ xs the vector to examine

Totality: total
Visibility: public export
mapProperty : (px->qx) ->Anypl->Anyql
Totality: total
Visibility: export
dataAll : (0_ : (a->Type)) ->Vectna->Type
  A proof that all elements of a vector satisfy a property. It is a list of
proofs, corresponding element-wise to the `Vect`.

Totality: total
Visibility: public export
Constructors:
Nil : Allp []
(::) : px->Allpxs->Allp (x::xs)

Hint: 
Either (Uninhabited (px)) (Uninhabited (Allpxs)) =>Uninhabited (Allp (x::xs))
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.

Totality: total
Visibility: export
notAllHere : Not (px) ->Not (Allp (x::xs))
Totality: total
Visibility: export
notAllThere : Not (Allpxs) ->Not (Allp (x::xs))
Totality: total
Visibility: export
all : ((x : a) ->Dec (px)) -> (xs : Vectna) ->Dec (Allpxs)
  Given a decision procedure for a property, decide whether all elements of
a vector satisfy it.

@ p the property
@ dec the decision procedure
@ xs the vector to examine

Totality: total
Visibility: public export
mapProperty : (px->qx) ->Allpl->Allql
Totality: total
Visibility: export
imapProperty : (0i : (Type->Type)) -> (ia=>pa->qa) ->Allitypes=>Allptypes->Allqtypes
Totality: total
Visibility: public export