Add missing test file (sorry!)
commit4a177a3723cf751ff657ca3f910fb8a7a1c9299f
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateSun 3 Apr 2016, 23:04 (11 years ago)
parentab385cd
test/proof011/proof011a.idrnew file+14
@@ -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