git.iko.soy/Idris-dev
on e2616ed help sign in
Idris-dev/test/proof011/expected
12 lines 473 B history raw
1proof011.idr:19:9:
2When checking right hand side of vassoc' with expected type
3 (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs
5rewrite did not change type x :: xs ++ ys ++ zs =
6 x :: (xs ++ ys) ++ zs
7proof011a.idr:13:9:
8When checking right hand side of vassoc' with expected type
9 (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs
11rewrite did not change type x :: xs ++ ys ++ zs =
12 x :: (xs ++ ys) ++ zs