Idris2/tests/idris2/reflection005/expected

15 lines
330 B
Plaintext
Raw Normal View History

1/1: Building refdecl (refdecl.idr)
Error: While processing right hand side of bad. When unifying Elab () and Elab a.
Mismatch between: () and a.
refdecl.idr:13:16--13:29
2021-02-11 20:24:26 +03:00
09 |
10 | %runElab mkDecls `(94)
11 |
12 | bad : a
2020-07-22 22:16:43 +03:00
13 | bad = %runElab mkDecls `(94)
2021-02-11 20:24:26 +03:00
^^^^^^^^^^^^^
Main> 9400
Main> Bye for now!