idris-1.3.3: test/proof011/expected.out
proof011.idr:20:7-21:18:
|
20 | = rewrite vassoc xs ys xs using vreplace in
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
When checking right hand side of vassoc' with expected type
(x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs
rewriting xs ++ ys ++ xs to (xs ++ ys) ++ xs did not change type x ::
xs ++
ys ++ zs =
x ::
(xs ++ ys) ++
zs
proof011a.idr:14:7-37:
|
14 | = rewrite vassoc xs ys xs in Refl
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking right hand side of vassoc' with expected type
(x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs
rewriting xs ++ ys ++ xs to (xs ++ ys) ++ xs did not change type x ::
xs ++
ys ++ zs =
x ::
(xs ++ ys) ++
zs