Idris2Doc : Data.Vect.Quantifiers

Data.Vect.Quantifiers

data All : (0 _ : (a -> Type)) -> Vect n a -> 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
Constructors:

Nil : All p []
(::) : p x -> All p xs -> All p (x :: xs)

data Any : (0 _ : (a -> Type)) -> Vect n a -> Type

  A proof that some element of a vector satisfies some property
  
  @ p the property to be satsified

Totality: total
Constructors:

Here : p x -> Any p (x :: xs)

  A proof that the satisfying element is the first one in the `Vect`

There : Any p xs -> Any p (x :: xs)

  A proof that the satsifying element is in the tail of the `Vect`

all : ((x : a) -> Dec (p x)) -> (xs : Vect n a) -> Dec (All p xs)

  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

any : ((x : a) -> Dec (p x)) -> (xs : Vect n a) -> Dec (Any p xs)

  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

anyElim : (Any p xs -> b) -> (p x -> b) -> Any p (x :: xs) -> b

  Eliminator for `Any`

Totality: total

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.

Totality: total

notAllHere : Not (p x) -> Not (All p (x :: xs))

Totality: total

notAllThere : Not (All p xs) -> Not (All p (x :: xs))

Totality: total