Open buzden opened 1 month ago
Consider I have a file Main.idr with the following contents:
Main.idr
namespace XX export main : IO () main = putStrLn "Hi, XX!" namespace YY export main : IO () main = putStrLn "Hi, YY!"
If we run
$ idris2 --exec main Main.idr
we expectedly get
Error: Ambiguous elaboration. Possible results: Main.XX.main Main.YY.main
Now, try to specify the namespace by running either
$ idris2 --exec YY.main Main.idr
or
$ idris2 --exec Main.YY.main Main.idr
Runs successfully and prints
Hi, YY!
or at least saying that namespaced main functions are not supported, if so.
Error: Undefined name YY.main.
and
Error: Undefined name Main.YY.main.
Steps to Reproduce
Consider I have a file
Main.idr
with the following contents:If we run
we expectedly get
Now, try to specify the namespace by running either
or
Expected Behavior
Runs successfully and prints
or at least saying that namespaced main functions are not supported, if so.
Observed Behavior
and