idris-0.9.18: test/tutorial006/expected
tutorial006a.idr:5:23-25:
When elaborating right hand side of vapp:
When elaborating argument xs to constructor Data.VectType.Vect.:::
Can't unify
Vect (n + n) a (Type of vapp xs xs)
with
Vect (plus n m) a (Expected type)
Specifically:
Can't unify
plus n n
with
plus n m
tutorial006b.idr:10:10:
When elaborating right hand side of with block in Main.parity:
Can't unify
Parity (plus (S j) (S j)) (Type of even)
with
Parity (S (S (plus j j))) (Expected type)
Specifically:
Can't unify
plus (S j) (S j)
with
S (S (plus j j))