Idris2Doc : Data.Vect.Properties.Fin

Data.Vect.Properties.Fin

dataNonEmpty : Vectna -> Type
  Witnesses non-empty runtime-irrelevant vectors. Analogous to Data.List.NonEmpty

Totality: total
Constructor: 
IsNonEmpty : NonEmpty (x::xs)
etaCons : (xs : Vect (Sn) a) -> headxs::tailxs = xs
  eta-law (extensionality) of head-tail cons

finNonEmpty : (0 xs : Vectna) -> NonZeron -> NonEmptyxs
  Inhabitants of `Fin n` witness runtime-irrelevant vectors of length `n` aren't empty

finNonZero : Finn -> NonZeron
  Inhabitants of `Fin n` witness `NonZero n`

finToElem : (0 xs : Vectna) -> (i : Finn) -> Elem (indexixs) xs
  Cast an index into a runtime-irrelevant `Vect` into the position
of the corresponding element

indexNaturalityWithElem : (i : Finn) -> (xs : Vectna) -> (f : ((x : a) -> (0 _ : Elemxxs) -> b)) -> indexi (mapWithElemxsf) = f (indexixs) (finToElemxsi)
  Analogus to `indexNaturality`, but morhisms can (irrelevantly) know the context