idris-1.3.3: test/meta003/expected.out
BadDef.idr:14:1-8:
|
14 | %runElab mkBadDef1
| ~~~~~~~~
While running an elaboration script, the following error occurred:
Type mismatch between
()
and
String
message error
unification error