Idris2Doc : Data.Vect.Properties.Fin



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

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

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

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

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

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

Visibility: export