Idris2Doc : Data.List.Views.Extra

Data.List.Views.Extra

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

  Totality: total
  Constructors:
  
BalancedZ : Balanced 0 0
  
BalancedL : Balanced 1 0
  
BalancedRec : Balanced n m -> Balanced (S n) (S m)
data LazyFilterRec : List a -> Type
  Lazy filtering of a list based on a predicate.

  Totality: total
  Constructors:
  
Exhausted : (skip : List a) -> LazyFilterRec skip
  
Found : (skip : List a) -> (head : a) -> Lazy (LazyFilterRec rest) -> LazyFilterRec (skip ++ (head :: rest))
data SplitBalanced : List a -> 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 (length xs) (length ys) -> SplitBalanced (xs ++ ys)
data VList : List a -> 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 (VList xs) -> VList (x :: (xs ++ [y]))
balancedPred : Balanced (S x) (S y) -> Balanced x y
  Totality: total
lazyFilterRec : (a -> Bool) -> (xs : List a) -> LazyFilterRec xs
  Covering function for the LazyFilterRec view.
  Constructs the view lazily in linear time.

  Totality: total
mkBalancedEq : n = m -> Balanced n m
  Totality: total
mkBalancedL : n = S m -> Balanced n m
  Totality: total
splitBalanced : (input : List a) -> SplitBalanced input
  Covering function for the `SplitBalanced`
  
  Constructs the view in linear time

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

  Totality: total