idris-1.3.3: test/tutorial006/expected.out
tutorial006a.idr:5:23-24:
|
5 | vapp (x :: xs) ys = x :: vapp xs xs -- BROKEN
| ~~
When checking right hand side of vapp with expected type
Vect (S len + m) a
When checking argument xs to constructor Data.Vect.:::
Type mismatch between
Vect (len + len) a (Type of vapp xs xs)
and
Vect (plus len m) a (Expected type)
Specifically:
Type mismatch between
plus len len
and
plus len m
tutorial006b.idr:10:39-50:
|
10 | parity (S (S (j + j))) | Even = Even {n=S j}
| ~~~~~~~~~~~~
When checking right hand side of with block in Main.parity with expected type
Parity (S (S (j + j)))
Type mismatch between
Parity (S j + S j) (Type of Even)
and
Parity (S (S (plus j j))) (Expected type)
Specifically:
Type mismatch between
plus (S j) (S j)
and
S (S (plus j j))