git.iko.soy/Idris-dev
on cd7e553 help sign in
Idris-dev/test/proof002/expected
21 lines 799 B history raw
1Reflect.idr:175:21-25:
2This style of tactic proof is deprecated. See %runElab for the replacement.
3Reflect.idr:184:21-25:
4This style of tactic proof is deprecated. See %runElab for the replacement.
5Reflect.idr:192:15-19:
6This style of tactic proof is deprecated. See %runElab for the replacement.
7test030a.idr:12:26-37:
8When checking right hand side of testReflect1 with expected type
9 ys ++ x :: ys ++ xs = (xs ++ [x]) ++ ys ++ xs
11When checking an application of function Reflect.getJust:
12 Type mismatch between
13 IsJust (Just x1) (Type of ItIsJust)
14 and
15 IsJust (prove (snd x)) (Expected type)
17 Specifically:
18 Type mismatch between
19 Just x
20 and
21 Nothing