git.iko.soy/Idris-dev
on master help sign in
Convention says the function should be 'vList'
ad473b3Edwin Brady
libs/base/Data/List/Views.idr+3−3
compare with master
unifiedsplit
@@ -210,9 +210,9 @@ toVList [] (Snoc {xs} {x} _) prf
210||| Covering function for `VList`
210||| Covering function for `VList`
211||| Constructs the view in linear time.
211||| Constructs the view in linear time.
212export
212export
213−vlist : (xs : List a) -> VList xs
213+vList : (xs : List a) -> VList xs
214−vlist xs with (splitBalanced xs)
214+vList xs with (splitBalanced xs)
215− vlist (ys ++ zs) | (MkSplitBal prf)
215+ vList (ys ++ zs) | (MkSplitBal prf)
216 = toVList ys (snocList zs) prf
216 = toVList ys (snocList zs) prf
217
217
218
218
test/views003/views003.idr+1−1
@@ -8,7 +8,7 @@ data Palindrome : List a -> Type where
8
8
9total
9total
10palindrome : DecEq a => (xs : List a) -> Maybe (Palindrome xs)
10palindrome : DecEq a => (xs : List a) -> Maybe (Palindrome xs)
11−palindrome xs with (vlist xs)
11+palindrome xs with (vList xs)
12 palindrome [] | VNil = Just PNil
12 palindrome [] | VNil = Just PNil
13 palindrome [x] | VOne = Just POne
13 palindrome [x] | VOne = Just POne
14 palindrome (x :: (ys ++ [y])) | (VCons z) with (decEq x y)
14 palindrome (x :: (ys ++ [y])) | (VCons z) with (decEq x y)