Data.Vect.Properties.Fin

Definitions

data NonEmpty : Vect n a -> Type

  Witnesses non-empty runtime-irrelevant vectors. Analogous to Data.List.NonEmpty

Totality: total
Visibility: public export
Constructor: 

IsNonEmpty : NonEmpty (x :: xs)

etaCons : (xs : Vect (S n) a) -> head xs :: tail xs = xs

  eta-law (extensionality) of head-tail cons

Visibility: export

finNonZero : Fin n -> NonZero n

  Inhabitants of `Fin n` witness `NonZero n`

Visibility: export

finNonEmpty : (0 xs : Vect n a) -> NonZero n -> NonEmpty xs

  Inhabitants of `Fin n` witness runtime-irrelevant vectors of length `n` aren't empty

Visibility: export

finToElem : (0 xs : Vect n a) -> (i : Fin n) -> Elem (index i xs) xs

  Cast an index into a runtime-irrelevant `Vect` into the position
  of the corresponding element

Visibility: public export

indexNaturalityWithElem : (i : Fin n) -> (xs : Vect n a) -> (f : ((x : a) -> (0 _ : Elem x xs) -> b)) -> index i (mapWithElem xs f) = f (index i xs) (finToElem xs i)

  Analogous to `indexNaturality`, but morphisms can (irrelevantly) know the context

Visibility: export