Idris2Doc : Data.Vect.Lens

Data.Vect.Lens

(source)
Reexports
import public Control.Lens
Definitions
reversed : Iso (Vect n a) (Vect n b) (Vect n a) (Vect n b)
  An isomorphism between a `Vect` and its reverse.

  Totality: total
  Visibility: public export
cons_ : Iso (Vect (S n) a) (Vect (S n) b) (a, Vect n a) (b, Vect n b)
  Totality: total
  Visibility: public export
head_ : Lens' (Vect (S n) a) a
  Totality: total
  Visibility: public export
tail_ : Lens' (Vect (S n) a) (Vect n a)
  Totality: total
  Visibility: public export
snoc_ : Iso (Vect (S n) a) (Vect (S n) b) (Vect n a, a) (Vect n b, b)
  Totality: total
  Visibility: public export
init_ : Lens' (Vect (S n) a) (Vect n a)
  Totality: total
  Visibility: public export
last_ : Lens' (Vect (S n) a) a
  Totality: total
  Visibility: public export