-
Notifications
You must be signed in to change notification settings - Fork 46
Open
Labels
bugSomething isn't workingSomething isn't working
Milestone
Description
Currently, agda2hs handles transitive imports by importing the names directly from the module where they were originally defined, ignoring any re-exporting layers in the Agda code. We should instead preserve the import structure that the user picked. Note that this would first require us to handle export lists (see #44), which are Haskell's way of doing public imports.
Metadata
Metadata
Assignees
Labels
bugSomething isn't workingSomething isn't working