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