git.iko.soy/Idris-dev
on 68c519e help sign in
Idris-dev/test/proof002/expected
19 lines 733 B history raw
1Reflect.idr:173:21-26:
2This style of tactic proof is deprecated. See %runElab for the replacement.
3Reflect.idr:182:21-26:
4This style of tactic proof is deprecated. See %runElab for the replacement.
5Reflect.idr:190: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:
9When checking an application of function Reflect.getJust:
10 Type mismatch between
11 IsJust (Just x1) (Type of ItIsJust)
12 and
13 IsJust (prove (getProof x)) (Expected type)
15 Specifically:
16 Type mismatch between
17 Just x
18 and
19 Nothing