Idris2Doc : Data.List.Views.Extra

Data.List.Views.Extra

dataBalanced : Nat -> Nat -> Type
  Proof that two numbers differ by at most one

Totality: total
Constructors:
BalancedZ : Balanced00
BalancedL : Balanced10
BalancedRec : Balancednm -> Balanced (Sn) (Sm)
dataLazyFilterRec : 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))
dataSplitBalanced : 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)
dataVList : 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 : VList []
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