git.iko.soy/Idris-dev
on master help sign in
Test update for hiding internal errors
f5974d9David Raymond Christiansen
test/test037/expected−14
compare with master
unifiedsplit
@@ -2,17 +2,3 @@ In file ErrorReflection.idr line 78 column 5
2 When elaborating right hand side of Main.bad :
2 When elaborating right hand side of Main.bad :
3 DSL type error: (t'(504) => t'(504)) doesn't match ()
3 DSL type error: (t'(504) => t'(504)) doesn't match ()
4
4
5−Original error:
6−
7− ErrorReflection.idr:78:5:When elaborating right hand side of bad:
8− Can't unify
9− Tm [] (Main.TFun t' t')
10− with
11− Tm [] Main.TUnit
12−
13− Specifically:
14− Can't unify
15− Main.TFun t' t'
16− with
17− Main.TUnit
18−