Idris2Doc : Data.Vect.Views.Extra

Data.Vect.Views.Extra

Additional views for Vect
dataSplit : Vectna -> Type
  View for splitting a vector in half, non-recursively

Totality: total
Constructors:
SplitNil : Split []
SplitOne : Split [x]
SplitPair : (x : a) -> (xs : Vectna) -> (y : a) -> (ys : Vectma) -> Split (x:: (xs++ (y::ys)))
  two non-empty parts
dataSplitRec : Vectka -> 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 (SplitRecxs) -> Lazy (SplitRecys) -> SplitRec (xs++ys)
split : (xs : Vectna) -> Splitxs
  Covering function for the `Split` view
Constructs the view in linear time

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

Totality: total