@@ -115,18 +115,12 @@ drop (S k) (x :: xs) = drop k xs
115115--------------------------------------------------------------------------------
116116
117117||| Reverse the order of the elements of a vector
118−total reverse : {n : Nat} -> Vect n a -> Vect n a
119−reverse {n} xs = reverse' [] (plusZeroRightNeutral n) xs
120− where
121− total reverse' : {m, j, l : Nat} ->
122− Vect m a -> (j + m = l) -> Vect j a -> Vect l a
123− reverse' {m} {j = Z } {l} acc prf [] ?= acc
124− reverse' {m} {j = S k} {l} acc prf (x::xs) =
125− let prf1 : (m + (S k) = l) = rewrite plusCommutative m (S k) in prf in
126− let prf2 : (S (m + k) = l) = rewrite plusSuccRightSucc m k in prf1 in
127− let prf3 : (S (k + m) = l) = rewrite plusCommutative k m in prf2 in
128− let prf4 : (k + (S m) = l) = rewrite sym $ plusSuccRightSucc k m in prf3 in
129− reverse' (x::acc) prf4 xs
118+reverse : Vect n a -> Vect n a
119+reverse xs = go [] xs
120+ where go : Vect n a -> Vect m a -> Vect (n+m) a
121+ go {n} acc [] = rewrite plusZeroRightNeutral n in acc
122+ go {n} {m=S m} acc (x :: xs) = rewrite sym $ plusSuccRightSucc n m
123+ in go (x::acc) xs
130124
131125||| Alternate an element between the other elements of a vector
132126||| @ sep the element to intersperse
@@ -487,13 +481,6 @@ vectAppendAssociative (x :: xs) ys zs =
487481-- Proofs
488482--------------------------------------------------------------------------------
489483
490−Prelude.Vect.reverse'_lemma_1 = proof {
491− intros;
492− rewrite prf;
493− rewrite sym (plusZeroRightNeutral m);
494− exact value;
495−}
496−
497484Prelude.Vect.intersperse'_lemma_1 = proof {
498485 intros;
499486 rewrite (plusSuccRightSucc n1 n1);