@@ -142,15 +142,13 @@ reverse = reverse' []
142142 reverse' acc [] ?= acc
143143 reverse' acc (x::xs) ?= reverse' (x::acc) xs
144144
145−total intersperse' : a -> Vect m a -> (p ** Vect p a)
146−intersperse' sep [] = (_ ** [])
147−intersperse' sep (y::ys) with (intersperse' sep ys)
148− | (_ ** tail) = (_ ** sep::y::tail)
149−
150−total intersperse : a -> Vect m a -> (p ** Vect p a)
151−intersperse sep [] = (_ ** [])
152−intersperse sep (x::xs) with (intersperse' sep xs)
153− | (_ ** tail) = (_ ** x::tail)
145+intersperse : a -> Vect n a -> Vect (n + pred n) a
146+intersperse sep [] = []
147+intersperse sep (x::xs) = x :: intersperse' sep xs
148+ where
149+ intersperse' : a -> Vect n a -> Vect (n + n) a
150+ intersperse' sep [] = []
151+ intersperse' sep (x::xs) ?= sep :: x :: intersperse' sep xs
154152
155153--------------------------------------------------------------------------------
156154-- Membership tests
@@ -328,3 +326,8 @@ Prelude.Vect.reverse'_lemma_1 = proof {
328326 exact value;
329327}
330328
329+Prelude.Vect.intersperse'_lemma_1 = proof {
330+ intros;
331+ rewrite (plusSuccRightSucc n1 n1);
332+ trivial;
333+}