git.iko.soy/Idris-dev
on 4efeda8 help sign in
Idris-dev/test/proof002/expected
37 lines 1.1 kB history raw
1Reflect.idr:175:21-25:
2 |
3175 | Reflect.appRExpr1 = proof {
4 | ~~~~~
5This style of tactic proof is deprecated. See %runElab for the replacement.
7Reflect.idr:184:21-25:
8 |
9184 | Reflect.appRExpr2 = proof {
10 | ~~~~~
11This style of tactic proof is deprecated. See %runElab for the replacement.
13Reflect.idr:192:15-19:
14 |
15192 | Reflect.bp1 = proof {
16 | ~~~~~
17This style of tactic proof is deprecated. See %runElab for the replacement.
19test030a.idr:12:26-37:
20 |
2112 | testReflect1 {a} xs ys = AssocProof a
22 | ~~~~~~~~~~~~
23When checking right hand side of testReflect1 with expected type
24 ys ++ x :: ys ++ xs = (xs ++ [x]) ++ ys ++ xs
26When checking an application of function Reflect.getJust:
27 Type mismatch between
28 IsJust (Just x1) (Type of ItIsJust)
29 and
30 IsJust (prove (snd x)) (Expected type)
32 Specifically:
33 Type mismatch between
34 Just x
35 and
36 Nothing