agda2hs
agda2hs copied to clipboard
Handle public imports properly
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 https://github.com/agda/agda2hs/issues/44), which are Haskell's way of doing public imports.