idris-0.9.19: test/proof002/expected
test030a.idr:12:26-14:1:
When checking right hand side of testReflect1:
When checking an application of function Reflect.getJust:
Type mismatch between
IsJust (Just x1) (Type of ItIsJust)
and
IsJust (prove (getProof x)) (Expected type)
Specifically:
Type mismatch between
Just x
and
Nothing