git.iko.soy/Idris-dev
on cf47310 help sign in
Idris-dev/test/tutorial006/expected
24 lines 759 B history raw
1tutorial006a.idr:5:23-25:When checking right hand side of vapp:
2When checking argument xs to constructor Data.VectType.Vect.:::
3 Type mismatch between
4 Vect (k + k) a (Type of vapp xs xs)
5 and
6 Vect (plus k m) a (Expected type)
7
8 Specifically:
9 Type mismatch between
10 plus k k
11 and
12 plus k m
13tutorial006b.idr:10:10:
14When checking right hand side of with block in Main.parity:
15Type mismatch between
16 Parity (plus (S j) (S j)) (Type of even)
17and
18 Parity (S (S (plus j j))) (Expected type)
20Specifically:
21 Type mismatch between
22 plus (S j) (S j)
23 and
24 S (S (plus j j))