git.iko.soy/Idris-dev
on ef51a46 help sign in
Idris-dev/test/proof011/expected
28 lines 1.4 kB history raw
1proof011.idr:20:7-21:18:
2 |
320 | = rewrite vassoc xs ys xs using vreplace in
4 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
5When checking right hand side of vassoc' with expected type
6 (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs
8rewriting xs ++ ys ++ xs to (xs ++ ys) ++ xs did not change type x ::
9 xs ++
10 ys ++ zs =
11 x ::
12 (xs ++ ys) ++
13 zs
15proof011a.idr:14:7-37:
16 |
1714 | = rewrite vassoc xs ys xs in Refl
18 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
19When checking right hand side of vassoc' with expected type
20 (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs
22rewriting xs ++ ys ++ xs to (xs ++ ys) ++ xs did not change type x ::
23 xs ++
24 ys ++ zs =
25 x ::
26 (xs ++ ys) ++
27 zs