git.iko.soy/Idris-dev
on master help sign in
Add missing test file (sorry!)
4a177a3Edwin Brady
test/proof011/proof011a.idrnew file+14
compare with master
unifiedsplit
@@ -0,0 +1,14 @@
1+import Data.Vect
2+
3+total
4+vassoc : (xs : Vect n a) -> (ys : Vect m a) -> (zs : Vect p a) ->
5+ xs ++ (ys ++ zs) = (xs ++ ys) ++ zs
6+vassoc [] ys zs = Refl
7+vassoc (x :: xs) ys zs
8+ = rewrite vassoc xs ys zs in Refl
9+total
10+vassoc' : (xs : Vect n a) -> (ys : Vect m a) -> (zs : Vect p a) ->
11+ xs ++ (ys ++ zs) = (xs ++ ys) ++ zs
12+vassoc' [] ys zs = Refl
13+vassoc' (x :: xs) ys zs
14+ = rewrite vassoc xs ys xs in Refl