Simplify the implementation of splitRec.
commit5b33b662eb80801a69d4758e753aa82a6dacc6bc
authorMatus Tejiscak <ziman@functor.sk>
dateThu 22 Jun 2017, 13:04 (9 years ago)
parent7e47b1d
libs/base/Data/List/Views.idr+2−2
@@ -71,8 +71,8 @@ splitRec xs with (sizeAccessible xs)
7171 splitRec [x] | acc | SplitOne = SplitRecOne
7272 splitRec (y :: ys ++ z :: zs) | Access acc | SplitPair
7373 = SplitRecPair
74− (splitRec (y :: ys) | acc (y :: ys) (smallerLeft ys z zs))
75− (splitRec (z :: zs) | acc (z :: zs) (smallerRight ys zs))
74+ (splitRec (y :: ys) | acc _ (smallerLeft ys z zs))
75+ (splitRec (z :: zs) | acc _ (smallerRight ys zs))
7676
7777||| View for traversing a list backwards
7878public export