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:

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

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

All (Uninhabited . p) xs => Uninhabited (Any p xs)

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 (DecEq . p) xs => DecEq (All p xs)

All (Eq . p) xs => Eq (Any 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 (Any p xs)

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

All (Uninhabited . p) xs => Uninhabited (Any p xs)

Either (Uninhabited (p x)) (Uninhabited (All p xs)) => Uninhabited (All 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

toDPair : Any p xs -> DPair a p

  Forget the membership proof

Totality: total
Visibility: public 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

anyToFinV : Any p xs -> (idx : Fin n ** p (index idx xs))

Totality: total
Visibility: public export

pushOut : Functor p => Any (p . q) xs -> p (Any q xs)

Totality: total
Visibility: public 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

consInjective : x :: xs = y :: ys -> (x = y, xs = ys)

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

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

  Take all but the first element.

Totality: total
Visibility: public 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

index : (i : Fin k) -> All p ts -> p (index i ts)

  Extract an element from an All.
  
  ```idris example
  > index 0 (the (HVect _) [1, "string"])
  1
  ```

Totality: total
Visibility: export

deleteAt : (i : Fin (S l)) -> All p ts -> All p (deleteAt i ts)

  Delete an element from an All at the given position.
  
  ```idris example
  > deleteAt 0 (the (HVect _) [1, "string"])
  ["string"]
  ```

Totality: total
Visibility: export

replaceAt : (i : Fin k) -> p t -> All p ts -> All p (replaceAt i t ts)

  Replace an element in an All at the given position.
  
  ```idris example
  > replaceAt 0 "firstString" (the (HVect _) [1, "string"])
  ["firstString", "string"]
  ```

Totality: total
Visibility: export

updateAt : (i : Fin k) -> (p (index i ts) -> p t) -> All p ts -> All p (replaceAt i t ts)

  Update an element in an All at the given position.
  
  ```idris example
  > updateAt 0 (const True) (the (HVect _) [1, "string"])
  [True, "string"]
  ```

Totality: total
Visibility: export

get : All p ts -> Elem x ts -> p x

  Extract an element of an All.
  
  ```idris example
  > get [1, "string"] {p = Here}
  1
  ```

Totality: total
Visibility: export

replaceElem : All p ts -> (e : Elem t ts) -> p t' -> All p (replaceByElem ts e t')

  Replace an element of an All.
  
  ```idris example
  > replaceElem 2 [1, "string"]
  [2, "string"]
  ```

Totality: total
Visibility: export

updateElem : (p t -> p t') -> All p ts -> (e : Elem t ts) -> All p (replaceByElem ts e t')

  Update an element of an All.
  
  ```idris example
  > updateElem (const "hello world!") [1, "string"]
  [1, "hello world!"]
  ```

Totality: total
Visibility: public export

pushIn : (xs : Vect n a) -> (0 _ : All p xs) -> Vect n (Subset a p)

  Push in the property from the list level with element level

Totality: total
Visibility: public export

pullOut : Vect n (Subset a p) -> Subset (Vect n a) (All p)

  Pull the elementwise property out to the list level

Totality: total
Visibility: public export

pushInOutInverse : (xs : Vect n a) -> (0 prf : All p xs) -> pullOut (pushIn xs prf) = Element xs prf

Totality: total
Visibility: export

pushOutInInverse : (xs : Vect n (Subset a p)) -> uncurry pushIn (pullOut xs) = xs

Totality: total
Visibility: export

pushOut : Applicative p => All (p . q) xs -> p (All q xs)

Totality: total
Visibility: public export

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

anyNegAll : Any (Not . p) xs -> Not (All p xs)

  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 (Any p xs)

  If none of the elements satisfy the property, then not any single one can.

Totality: total
Visibility: export

allAnies : All p xs -> Vect n (Any p xs)

Totality: total
Visibility: public export

altAll : Alternative p => All (p . q) xs -> p (Any q xs)

Totality: total
Visibility: public export