Idris2Doc : Data.Vect.Views.Extra

Data.Vect.Views.Extra

Additional views for Vect

Definitions

dataSplit : Vectna->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 : Vectna) -> (y : a) -> (ys : Vectma) ->Split (x:: (xs++ (y::ys)))
  two non-empty parts
split : (xs : Vectna) ->Splitxs
  Covering function for the `Split` view
Constructs the view in linear time

Totality: total
Visibility: export
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
Visibility: public export
Constructors:
SplitRecNil : SplitRec []
SplitRecOne : SplitRec [x]
SplitRecPair : Lazy (SplitRecxs) -> Lazy (SplitRecys) ->SplitRec (xs++ys)
splitRec : (xs : Vectka) ->SplitRecxs
  Covering function for the `SplitRec` view
Constructs the view in O(n lg n)

Totality: total
Visibility: public export