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