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