idris-1.3.0: test/meta003/expected
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
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