Data.Vect.Views.Extra

Additional views for Vect

Definitions

data Split : Vect n a -> Type

  View for splitting a vector in half, non-recursively

Totality: total
Visibility: public export
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

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

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

Totality: total
Visibility: export

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
Visibility: public export
Constructors:

SplitRecNil : SplitRec []

SplitRecOne : SplitRec [x]

SplitRecPair : Lazy (SplitRec xs) -> Lazy (SplitRec ys) -> SplitRec (xs ++ ys)

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

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

Totality: total
Visibility: public export