git.iko.soy/Idris-dev
on fdfcdd3 help sign in
Idris-dev/test/proof011/expected
18 lines 1.1 kB history raw
1proof011.idr:19:9:When checking right hand side of vassoc' with expected type
2 (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs
4rewriting xs ++ ys ++ xs to (xs ++ ys) ++ xs did not change type x ::
5 xs ++
6 ys ++ zs =
7 x ::
8 (xs ++ ys) ++
9 zs
10proof011a.idr:13:9:When checking right hand side of vassoc' with expected type
11 (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs
13rewriting xs ++ ys ++ xs to (xs ++ ys) ++ xs did not change type x ::
14 xs ++
15 ys ++ zs =
16 x ::
17 (xs ++ ys) ++
18 zs