Idris2Doc : Data.List.Views.Extra

Data.List.Views.Extra

Balanced : Nat -> Nat -> Type
Proof that two numbers differ by at most one
Totality: total
Constructors:
BalancedZ : BalancedZZ
BalancedL : Balanced 1 Z
BalancedRec : Balancednm -> Balanced (Sn) (Sm)
LazyFilterRec : Lista -> Type
Lazy filtering of a list based on a predicate.
Totality: total
Constructors:
Exhausted : (skip : Lista) -> LazyFilterRecskip
Found : (skip : Lista) -> (head : a) -> Lazy (LazyFilterRecrest) -> LazyFilterRec (skip++ (head::rest))
SplitBalanced : Lista -> Type
View of a list split into two halves

The lengths of the lists are guaranteed to differ by at most one
Totality: total
Constructor: 
MkSplitBal : Balanced (lengthxs) (lengthys) -> SplitBalanced (xs++ys)
VList : Lista -> Type
The `VList` view allows us to recurse on the middle of a list,
inspecting the front and back elements simultaneously.
Totality: total
Constructors:
VNil : VListNil
VOne : VList [x]
VCons : Lazy (VListxs) -> VList (x:: (xs++ [y]))
balancedPred : Balanced (Sx) (Sy) -> Balancedxy
Totality: total
lazyFilterRec : (a -> Bool) -> (xs : Lista) -> LazyFilterRecxs
Covering function for the LazyFilterRec view.
Constructs the view lazily in linear time.
Totality: total
mkBalancedEq : n = m -> Balancednm
Totality: total
mkBalancedL : n = Sm -> Balancednm
Totality: total
splitBalanced : (input : Lista) -> SplitBalancedinput
Covering function for the `SplitBalanced`

Constructs the view in linear time
Totality: total
vList : (xs : Lista) -> VListxs
Covering function for `VList`
Constructs the view in linear time.
Totality: total