idris-0.9.17: test/proof002/expected
Reflect.idr:208:38:
When elaborating right hand side of testReflect1:
When elaborating an application of function Reflect.getJust:
Can't unify
IsJust (Just x1) (Type of ItIsJust)
with
IsJust (prove (getProof x)) (Expected type)
Specifically:
Can't unify
Just x
with
Nothing