Idris2Doc : Data.List.Views

Data.List.Views

SnocList : Lista -> Type
View for traversing a list backwards
Totality: total
Constructors:
Empty : SnocListNil
Snoc : (x : a) -> (xs : Lista) -> SnocListxs -> SnocList (xs++ [x])
Split : Lista -> Type
View for splitting a list in half, non-recursively
Totality: total
Constructors:
SplitNil : SplitNil
SplitOne : (x : a) -> Split [x]
SplitPair : (x : a) -> (xs : Lista) -> (y : a) -> (ys : Lista) -> Split (x:: (xs++ (y::ys)))
SplitRec : Lista -> Type
Totality: total
Constructors:
SplitRecNil : SplitRecNil
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