@@ -142,15 +142,13 @@ reverse = reverse' []
142 reverse' acc [] ?= acc
142 reverse' acc [] ?= acc
143 reverse' acc (x::xs) ?= reverse' (x::acc) xs
143 reverse' acc (x::xs) ?= reverse' (x::acc) xs
145−total intersperse' : a -> Vect m a -> (p ** Vect p a)
145+intersperse : a -> Vect n a -> Vect (n + pred n) a
146−intersperse' sep [] = (_ ** [])
146+intersperse sep [] = []
147−intersperse' sep (y::ys) with (intersperse' sep ys)
147+intersperse sep (x::xs) = x :: intersperse' sep xs
148− | (_ ** tail) = (_ ** sep::y::tail)
148+ where
150−total intersperse : a -> Vect m a -> (p ** Vect p a)
149+ intersperse' : a -> Vect n a -> Vect (n + n) a
151−intersperse sep [] = (_ ** [])
150+ intersperse' sep [] = []
152−intersperse sep (x::xs) with (intersperse' sep xs)
151+ intersperse' sep (x::xs) ?= sep :: x :: intersperse' sep xs
153− | (_ ** tail) = (_ ** x::tail)
155--------------------------------------------------------------------------------
153--------------------------------------------------------------------------------
156-- Membership tests
154-- Membership tests
@@ -328,3 +326,8 @@ Prelude.Vect.reverse'_lemma_1 = proof {
328 exact value;
326 exact value;
329+Prelude.Vect.intersperse'_lemma_1 = proof {
331+ rewrite (plusSuccRightSucc n1 n1);