packages feed

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))