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