Data.Vect.Quantifiers

Definitions

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
Visibility: public export
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`

Hints:

Uninhabited (Any p [])

Uninhabited (p x) => Uninhabited (Any p xs) => Uninhabited (Any p (x :: xs))

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

  Eliminator for `Any`

Totality: total
Visibility: public export

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
Visibility: public export

mapProperty : (p x -> q x) -> Any p l -> Any q l

Totality: total
Visibility: export

toExists : Any p xs -> Exists p

Totality: total
Visibility: export

anyToFin : Any p xs -> Fin n

  Get the bounded numeric position of the element satisfying the predicate

Totality: total
Visibility: public export

anyToFinCorrect : (witness : Any p xs) -> p (index (anyToFin witness) xs)

  `anyToFin`'s return type satisfies the predicate

Totality: total
Visibility: export

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
Visibility: public export
Constructors:

Nil : All p []

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

Hints:

All (Ord . p) xs => All (Eq . p) xs

All (Monoid . p) xs => All (Semigroup . p) xs

All (Eq . p) xs => Eq (All p xs)

All (Monoid . p) xs => Monoid (All p xs)

All (Ord . p) xs => Ord (All p xs)

All (Semigroup . p) xs => Semigroup (All p xs)

All (Show . p) xs => Show (All p xs)

Either (Uninhabited (p x)) (Uninhabited (All p xs)) => Uninhabited (All p (x :: xs))

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
Visibility: export

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

Totality: total
Visibility: export

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

Totality: total
Visibility: export

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
Visibility: public export

mapProperty : (p x -> q x) -> All p l -> All q l

Totality: total
Visibility: export

mapPropertyRelevant : ((x : a) -> p x -> q x) -> All p xs -> All q xs

  A variant of `mapProperty` that also allows accessing
  the values of `xs` that the corresponding `ps` prove `p` about.

Totality: total
Visibility: export

imapProperty : (0 i : (a -> Type)) -> (i x => p x -> q x) -> All i as => All p as -> All q as

Totality: total
Visibility: public export

forget : All (const p) xs -> Vect n p

  If `All` witnesses a property that does not depend on the vector `xs`
  it's indexed by, then it is really a `Vect`.

Totality: total
Visibility: public export

remember : (xs : Vect n ty) -> All (const ty) xs

  Any `Vect` can be lifted to become an `All`
  witnessing the presence of elements of the `Vect`'s type.

Totality: total
Visibility: public export

forgetRememberId : (xs : Vect n ty) -> forget (remember xs) = xs

Totality: total
Visibility: export

castAllConst : All (const ty) xs -> All (const ty) ys

Totality: total
Visibility: public export

rememberForgetId : (vs : All (const ty) xs) -> castAllConst (remember (forget vs)) = vs

Totality: total
Visibility: export

zipPropertyWith : (p x -> q x -> r x) -> All p xs -> All q xs -> All r xs

Totality: total
Visibility: export

traverseProperty : Applicative f => (p x -> f (q x)) -> All p xs -> f (All q xs)

  A `Traversable`'s `traverse` for `All`,
  for traversals that don't care about the values of the associated `Vect`.

Totality: total
Visibility: export

traversePropertyRelevant : Applicative f => ((x : a) -> p x -> f (q x)) -> All p xs -> f (All q xs)

  A `Traversable`'s `traverse` for `All`,
  in case the elements of the `Vect` that the `All` is proving `p` about are also needed.

Totality: total
Visibility: export

tabulate : ((ix : Fin n) -> p (index ix xs)) -> All p xs

Totality: total
Visibility: public export

(++) : All p xs -> All p ys -> All p (xs ++ ys)

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7

HVect : Vect n Type -> Type

  A heterogeneous vector of arbitrary types

Totality: total
Visibility: public export

head : All p (x :: xs) -> p x

  Take the first element.

Totality: total
Visibility: export

tail : All p (x :: xs) -> All p xs

  Take all but the first element.

Totality: total
Visibility: export

drop : (n : Nat) -> All p xs -> All p (the (Vect m a) (drop n xs))

  Drop the first n elements given knowledge that
  there are at least n elements available.

Totality: total
Visibility: export

drop' : (l : Nat) -> All p xs -> All p (drop' l xs)

  Drop up to the first l elements, stopping early
  if all elements have been dropped.

Totality: total
Visibility: export