Data.List.Views

Definitions

data Split : List a -> Type

  View for splitting a list in half, non-recursively

Totality: total
Visibility: public export
Constructors:

SplitNil : Split []

SplitOne : (x : a) -> Split [x]

SplitPair : (x : a) -> (xs : List a) -> (y : a) -> (ys : List a) -> Split (x :: (xs ++ (y :: ys)))

split : (xs : List a) -> Split xs

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

Totality: total
Visibility: export

data SplitRec : List a -> Type

Totality: total
Visibility: public export
Constructors:

SplitRecNil : SplitRec []

SplitRecOne : (x : a) -> SplitRec [x]

SplitRecPair : (lefts : List a) -> (rights : List a) -> Lazy (SplitRec lefts) -> Lazy (SplitRec rights) -> SplitRec (lefts ++ rights)

splitRec : (xs : List a) -> SplitRec xs

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

Totality: total
Visibility: public export

data SnocList : List a -> Type

  View for traversing a list backwards

Totality: total
Visibility: public export
Constructors:

Empty : SnocList []

Snoc : (x : a) -> (xs : List a) -> SnocList xs -> SnocList (xs ++ [x])

snocList : (xs : List a) -> SnocList xs

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

Totality: total
Visibility: export