- data SnocList : List a -> Type
View for traversing a list backwards
Totality: total
Constructors:
- Empty : SnocList []
- Snoc : (x : a) -> (xs : List a) -> SnocList xs -> SnocList (xs ++ [x])
- data Split : List a -> Type
View for splitting a list in half, non-recursively
Totality: total
Constructors:
- SplitNil : Split []
- SplitOne : (x : a) -> Split [x]
- SplitPair : (x : a) -> (xs : List a) -> (y : a) -> (ys : List a) -> Split (x :: (xs ++ (y :: ys)))
- data SplitRec : List a -> Type
- Totality: total
Constructors:
- SplitRecNil : SplitRec []
- SplitRecOne : (x : a) -> SplitRec [x]
- SplitRecPair : (lefts : List a) -> (rights : List a) -> Lazy (SplitRec lefts) -> Lazy (SplitRec rights) -> SplitRec (lefts ++ rights)
- snocList : (xs : List a) -> SnocList xs
Covering function for the `SnocList` view
Constructs the view in linear time
Totality: total- split : (xs : List a) -> Split xs
Covering function for the `Split` view
Constructs the view in linear time
Totality: total- splitRec : (xs : List a) -> SplitRec xs
Covering function for the `SplitRec` view
Constructs the view in O(n lg n)
Totality: total