git.iko.soy/Idris-dev
on 0222012 help sign in
Idris-dev/test/proof002/expected
21 lines 801 B history raw
1Reflect.idr:174:21-26:
2This style of tactic proof is deprecated. See %runElab for the replacement.
3Reflect.idr:183:21-26:
4This style of tactic proof is deprecated. See %runElab for the replacement.
5Reflect.idr:191:15-20:
6This style of tactic proof is deprecated. See %runElab for the replacement.
7test030a.idr:12:26-14:1:
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