Data.List.Views.Extra

Definitions

data Balanced : Nat -> Nat -> Type

  Proof that two numbers differ by at most one

Totality: total
Visibility: public export
Constructors:

BalancedZ : Balanced 0 0

BalancedL : Balanced 1 0

BalancedRec : Balanced n m -> Balanced (S n) (S m)

Hint: 

Uninhabited (Balanced 0 (S k))

balancedPred : Balanced (S x) (S y) -> Balanced x y

Totality: total
Visibility: export

mkBalancedEq : n = m -> Balanced n m

Totality: total
Visibility: export

mkBalancedL : n = S m -> Balanced n m

Totality: total
Visibility: export

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
Visibility: public export
Constructor: 

MkSplitBal : Balanced (length xs) (length ys) -> SplitBalanced (xs ++ ys)

splitBalanced : (input : List a) -> SplitBalanced input

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

Totality: total
Visibility: export

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
Visibility: public export
Constructors:

VNil : VList []

VOne : VList [x]

VCons : Lazy (VList xs) -> VList (x :: (xs ++ [y]))

vList : (xs : List a) -> VList xs

  Covering function for `VList`
  Constructs the view in linear time.

Totality: total
Visibility: export

data LazyFilterRec : List a -> Type

  Lazy filtering of a list based on a predicate.

Totality: total
Visibility: public export
Constructors:

Exhausted : (skip : List a) -> LazyFilterRec skip

Found : (skip : List a) -> (head : a) -> Lazy (LazyFilterRec rest) -> LazyFilterRec (skip ++ (head :: rest))

lazyFilterRec : (a -> Bool) -> (xs : List a) -> LazyFilterRec xs

  Covering function for the LazyFilterRec view.
  Constructs the view lazily in linear time.

Totality: total
Visibility: export