git.iko.soy/Idris-dev
on master help sign in
Fix tests due to name change
6f904d5Edwin Brady
test/proof001/test029.idr+1−1
compare with master
unifiedsplit
@@ -29,7 +29,7 @@ append (x :: xs) ys ?= x :: append xs ys
29simple.append_lemma_2 = proof {
29simple.append_lemma_2 = proof {
30 intros;
30 intros;
31 compute;
31 compute;
32− rewrite (plusSuccRightSucc m n);
32+ rewrite (plusSuccRightSucc m k);
33 trivial;
33 trivial;
34}
34}
35
35
test/tutorial006/expected+4−4
@@ -1,15 +1,15 @@
1tutorial006a.idr:5:23-25:When checking right hand side of vapp:
1tutorial006a.idr:5:23-25:When checking right hand side of vapp:
2When checking argument xs to constructor Data.VectType.Vect.:::
2When checking argument xs to constructor Data.VectType.Vect.:::
3 Type mismatch between
3 Type mismatch between
4− Vect (n + n) a (Type of vapp xs xs)
4+ Vect (k + k) a (Type of vapp xs xs)
5 and
5 and
6− Vect (plus n m) a (Expected type)
6+ Vect (plus k m) a (Expected type)
7
7
8 Specifically:
8 Specifically:
9 Type mismatch between
9 Type mismatch between
10− plus n n
10+ plus k k
11 and
11 and
12− plus n m
12+ plus k m
13tutorial006b.idr:10:10:
13tutorial006b.idr:10:10:
14When checking right hand side of with block in Main.parity:
14When checking right hand side of with block in Main.parity:
15Type mismatch between
15Type mismatch between