git.iko.soy/Idris-dev
on 239c8ca help sign in
Idris-dev/test/proof002/expected
13 lines 436 B history raw
1test030a.idr:12:26-14:1:
2When checking right hand side of testReflect1:
3When checking an application of function Reflect.getJust:
4 Type mismatch between
5 IsJust (Just x1) (Type of ItIsJust)
6 and
7 IsJust (prove (getProof x)) (Expected type)
8
9 Specifically:
10 Type mismatch between
11 Just x
12 and
13 Nothing