Idris2Doc : Data.List.Views

Data.List.Views

dataSnocList : Lista -> Type
  View for traversing a list backwards

Totality: total
Constructors:
Empty : SnocList []
Snoc : (x : a) -> (xs : Lista) -> SnocListxs -> SnocList (xs++ [x])
dataSplit : Lista -> Type
  View for splitting a list in half, non-recursively

Totality: total
Constructors:
SplitNil : Split []
SplitOne : (x : a) -> Split [x]
SplitPair : (x : a) -> (xs : Lista) -> (y : a) -> (ys : Lista) -> Split (x:: (xs++ (y::ys)))
dataSplitRec : Lista -> Type
Totality: total
Constructors:
SplitRecNil : SplitRec []
SplitRecOne : (x : a) -> SplitRec [x]
SplitRecPair : (lefts : Lista) -> (rights : Lista) -> Lazy (SplitReclefts) -> Lazy (SplitRecrights) -> SplitRec (lefts++rights)
snocList : (xs : Lista) -> SnocListxs
  Covering function for the `SnocList` view
Constructs the view in linear time

Totality: total
split : (xs : Lista) -> Splitxs
  Covering function for the `Split` view
Constructs the view in linear time

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

Totality: total