Fix tests due to name change
commit6f904d5adfa91c1c22d4ab66208947450cd97a60
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateSun 9 Aug 2015, 16:34 (11 years ago)
parentbf6c327
test/proof001/test029.idr+1−1
@@ -29,7 +29,7 @@ append (x :: xs) ys ?= x :: append xs ys
2929simple.append_lemma_2 = proof {
3030 intros;
3131 compute;
32− rewrite (plusSuccRightSucc m n);
32+ rewrite (plusSuccRightSucc m k);
3333 trivial;
3434}
3535
test/tutorial006/expected+4−4
@@ -1,15 +1,15 @@
11tutorial006a.idr:5:23-25:When checking right hand side of vapp:
22When checking argument xs to constructor Data.VectType.Vect.:::
33 Type mismatch between
4− Vect (n + n) a (Type of vapp xs xs)
4+ Vect (k + k) a (Type of vapp xs xs)
55 and
6− Vect (plus n m) a (Expected type)
6+ Vect (plus k m) a (Expected type)
77
88 Specifically:
99 Type mismatch between
10− plus n n
10+ plus k k
1111 and
12− plus n m
12+ plus k m
1313tutorial006b.idr:10:10:
1414When checking right hand side of with block in Main.parity:
1515Type mismatch between