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