idris-0.9.19.1: test/tutorial006/expected
tutorial006a.idr:5:23-25:When checking right hand side of vapp:
When checking argument xs to constructor Data.Vect.:::
Type mismatch between
Vect (k + k) a (Type of vapp xs xs)
and
Vect (plus k m) a (Expected type)
Specifically:
Type mismatch between
plus k k
and
plus k m
tutorial006b.idr:10:10:
When checking right hand side of with block in Main.parity:
Type mismatch between
Parity (plus (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))