IdrisDoc: Data.Vect.Views

Data.Vect.Views

data SnocVect : Vect n a -> Type

View for traversing a vector backwards

Empty : SnocVect []
Snoc : (rec : SnocVect xs) -> SnocVect (xs ++ [x])
data Split : Vect n a -> Type

View for splitting a vector in half, non-recursively

SplitNil : Split []
SplitOne : Split [x]
SplitPair : Split (x :: xs ++ y :: ys)
data SplitRec : Vect n a -> Type

View for splitting a vector in half, recursively

This allows us to define recursive functions which repeatedly split vectors
in half, with base cases for the empty and singleton lists.

SplitRecNil : SplitRec []
SplitRecOne : SplitRec [x]
SplitRecPair : (lrec : Lazy (SplitRec xs)) -> (rrec : Lazy (SplitRec ys)) -> SplitRec (xs ++ ys)
snocVect : (xs : Vect n a) -> SnocVect xs

Covering function for the SnocVect view
Constructs the view in linear time

split : (xs : Vect n a) -> Split xs

Covering function for the Split view
Constructs the view in linear time

splitRec : (xs : Vect n a) -> SplitRec xs

Covering function for the SplitRec view
Constructs the view in O(n lg n)