Idris2Doc : Data.List.Views

Data.List.Views

Definitions

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

Totality: total
Visibility: export
dataSplitRec : Lista->Type
Totality: total
Visibility: public export
Constructors:
SplitRecNil : SplitRec []
SplitRecOne : (x : a) ->SplitRec [x]
SplitRecPair : (lefts : Lista) -> (rights : Lista) -> Lazy (SplitReclefts) -> Lazy (SplitRecrights) ->SplitRec (lefts++rights)
splitRec : (xs : Lista) ->SplitRecxs
  Covering function for the `SplitRec` view
Constructs the view in O(n lg n)

Totality: total
Visibility: public export
dataSnocList : Lista->Type
  View for traversing a list backwards

Totality: total
Visibility: public export
Constructors:
Empty : SnocList []
Snoc : (x : a) -> (xs : Lista) ->SnocListxs->SnocList (xs++ [x])
snocList : (xs : Lista) ->SnocListxs
  Covering function for the `SnocList` view
Constructs the view in linear time

Totality: total
Visibility: export