git.iko.soy/Idris-dev
on master help sign in
Convention says the function should be 'vList'
commitad473b396d452f184bbcf7eca78f2345caa809b6 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 12 Apr 2016, 16:41 (11 years ago) parent069a2ac
2 files changed+4−4
compare with master
unifiedsplit
libs/base/Data/List/Views.idr+3−3 test/views003/views003.idr+1−1
libs/base/Data/List/Views.idr+3−3
@@ -210,9 +210,9 @@ toVList [] (Snoc {xs} {x} _) prf
210210||| Covering function for `VList`
211211||| Constructs the view in linear time.
212212export
213−vlist : (xs : List a) -> VList xs
214−vlist xs with (splitBalanced xs)
215− vlist (ys ++ zs) | (MkSplitBal prf)
213+vList : (xs : List a) -> VList xs
214+vList xs with (splitBalanced xs)
215+ vList (ys ++ zs) | (MkSplitBal prf)
216216 = toVList ys (snocList zs) prf
217217
218218
test/views003/views003.idr+1−1
@@ -8,7 +8,7 @@ data Palindrome : List a -> Type where
88
99total
1010palindrome : DecEq a => (xs : List a) -> Maybe (Palindrome xs)
11−palindrome xs with (vlist xs)
11+palindrome xs with (vList xs)
1212 palindrome [] | VNil = Just PNil
1313 palindrome [x] | VOne = Just POne
1414 palindrome (x :: (ys ++ [y])) | (VCons z) with (decEq x y)