@@ -138,12 +138,17 @@ lsplit (x :: xs) (S k) prf (S l) right prf1
138138 (x :: lsrec' ** rsrec' ** (eqSucc _ _ lprf, rprf, rewrite recprf in Refl))
139139lsplit (_ :: _) Z Refl (S _) _ _ impossible
140140
141+||| Proof that two numbers differ by at most one
142+public export
141143data Balanced : Nat -> Nat -> Type where
142144 BalancedZ : Balanced Z Z
143145 BalancedL : Balanced (S Z) Z
144146 BalancedRec : Balanced n m -> Balanced (S n) (S m)
145147
146−-- Question: worth exporting?
148+||| View of a list split into two halves
149+|||
150+||| The lengths of the lists are guaranteed to differ by at most one
151+public export
147152data SplitBalanced : List a -> Type where
148153 MkSplitBal : {xs, ys : List a} ->
149154 Balanced (length xs) (length ys) -> SplitBalanced (xs ++ ys)
@@ -168,6 +173,10 @@ splitBalancedLen xs n prf with (half n)
168173 lsplit xs (x + x) prf x x Refl in
169174 rewrite apprf in (MkSplitBal (mkBalanced lprf rprf))
170175
176+||| Covering function for the `SplitBalanced`
177+|||
178+||| Constructs the view in linear time
179+export
171180splitBalanced : (xs : List a) -> SplitBalanced xs
172181splitBalanced xs = splitBalancedLen xs (length xs) Refl
173182