git.iko.soy/Idris-dev
on cfd6dbc help sign in
Idris-dev/test/proof002/expected
12 lines 418 B history raw
1Reflect.idr:208:38:When elaborating right hand side of testReflect1:
2When elaborating an application of function Reflect.getJust:
3 Can't unify
4 IsJust (Just x1) (Type of ItIsJust)
5 with
6 IsJust (prove (getProof x)) (Expected type)
7
8 Specifically:
9 Can't unify
10 Just x
11 with
12 Nothing