Spidr.Data.Vect

Vect definitions.

Reexports

Definitions

range : (n : Nat) -> Vect n Nat

  All numbers from `0` to `n - 1` inclusive, in increasing order.
  
  @n The (exclusive) limit of the range.

Totality: total
Visibility: export

enumerate : Vect n a -> Vect n (Nat, a)

  Enumerate entries in a vector with their indices. For example, `enumerate [5, 7, 9]`
  is `[(0, 5), (1, 7), (2, 9)]`.

Totality: total
Visibility: export

functorIdentity : (xs : Vect n a) -> map id xs = xs

Totality: total
Visibility: public export