@@ -130,8 +130,9 @@ intersperse sep [] = []
130130intersperse sep (x::xs) = x :: intersperse' sep xs
131131 where
132132 intersperse' : a -> Vect n a -> Vect (n + n) a
133− intersperse' sep [] = []
134− intersperse' sep (x::xs) ?= sep :: x :: intersperse' sep xs
133+ intersperse' sep [] = []
134+ intersperse' {n=S n} sep (x::xs) = rewrite sym $ plusSuccRightSucc n n
135+ in sep :: x :: intersperse' sep xs
135136
136137--------------------------------------------------------------------------------
137138-- Conversion from list (toList is provided by Foldable)
@@ -486,12 +487,3 @@ vectAppendAssociative (x :: xs) ys zs =
486487 vectConsCong _ _ _ (vectAppendAssociative xs ys zs)
487488
488489
489−--------------------------------------------------------------------------------
490−-- Proofs
491−--------------------------------------------------------------------------------
492−
493−Prelude.Vect.intersperse'_lemma_1 = proof {
494− intros;
495− rewrite (plusSuccRightSucc n1 n1);
496− trivial;
497−}