Idris2Doc : Data.Vect.Views.Extra

Data.Vect.Views.Extra

Additional views for Vect
data Split : Vect n a -> Type
  View for splitting a vector in half, non-recursively

Totality: total
Constructors:
SplitNil : Split []
SplitOne : Split [x]
SplitPair : (x : a) -> (xs : Vect n a) -> (y : a) -> (ys : Vect m a) -> Split (x :: (xs ++ (y :: ys)))
  two non-empty parts
data SplitRec : Vect k 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.

Totality: total
Constructors:
SplitRecNil : SplitRec []
SplitRecOne : SplitRec [x]
SplitRecPair : Lazy (SplitRec xs) -> Lazy (SplitRec ys) -> SplitRec (xs ++ ys)
split : (xs : Vect n a) -> Split xs
  Covering function for the `Split` view
  Constructs the view in linear time

Totality: total
splitRec : (xs : Vect k a) -> SplitRec xs
  Covering function for the `SplitRec` view
  Constructs the view in O(n lg n)

Totality: total