test/tutorial006/expected · Idris-dev

git.iko.soy/Idris-dev

on 4e34dfd help sign in

23 lines 1.1 kB history raw

1tutorial006a.idr:5:23:When elaborating right hand side of vapp:

2When elaborating argument [95mxs[0m to constructor [91mData.VectType.Vect.::[0m:

3 Can't unify

4 [94mVect[0m ([95mn[0m [92m+[0m [95mn[0m) [95ma[0m (Type of vapp [95mxs[0m [95mxs[0m)

5 with

6 [94mVect[0m ([92mplus[0m [95mn[0m [95mm[0m) [95ma[0m (Expected type)

8 Specifically:

9 Can't unify

10 [92mplus[0m [95mn[0m [95mn[0m

11 with

12 [92mplus[0m [95mn[0m [95mm[0m

13tutorial006b.idr:10:10:When elaborating right hand side of with block in Main.parity:

14Can't unify

15 [94mParity[0m ([92mplus[0m ([91mS[0m [95mj[0m) ([91mS[0m [95mj[0m)) (Type of [91meven[0m)

16with

17 [94mParity[0m ([91mS[0m ([91mS[0m ([92mplus[0m [95mj[0m [95mj[0m))) (Expected type)

19Specifically:

20 Can't unify

21 [92mplus[0m ([91mS[0m [95mj[0m) ([91mS[0m [95mj[0m)

22 with

23 [91mS[0m ([91mS[0m ([92mplus[0m [95mj[0m [95mj[0m))