agda2hs icon indicating copy to clipboard operation
agda2hs copied to clipboard

Handle public imports properly

Open jespercockx opened this issue 2 years ago • 0 comments

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.

jespercockx avatar Nov 14 '22 11:11 jespercockx