Compile reexport of individual items
Maintainers usually reply within 1 day
@wasabi315 is already working on this.
Since Nov 4, 2026.
Assessment
This issue has not been assessed yet.
Description
Compile reexport of individual items.
Example:
module M where
open import M1 public using (foo)
open import M2 public hiding (bar)
module M (foo, module M2) where
import M1 (foo)
import M2 hiding (bar)
Things to consider:
- Reexport of items with
COMPILE to. Automatically translate into reexport of the target? - Reexport of items subject to rewrite rules. Automatically translate into reexport of the target?
- Dominant language
- Agda
- Stars
- 211
- Forks
- 51
- Avg merge
- 1d 11h
- Merged PRs (30d)
- 9
Getting set up
This project ships no dev container, Dockerfile or contributing guide, so setting up is up to you: start from its README, and see our first-contribution guide for the general steps.
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from agda/agda2hs
-
Refine the fix of #142Possibly taken @jespercockx claimed this 1 day ago. Openenhancement
agda/agda2hs#494 · 1 assignee ·
Maintainers usually reply within 1 day
-
enhancement
Difficulty 5/5 Over a week Newbie friendliness 8/100
Maintainers usually reply within 1 day
-
bug library
Difficulty 4/5 3-5 days Newbie friendliness 45/100
agda/agda2hs#488 · 1 comment ·
Maintainers usually reply within 1 day
-
bug library
Difficulty 4/5 3-5 days Newbie friendliness 49/100
agda/agda2hs#487 · 3 comments ·
Maintainers usually reply within 1 day
-
Skipping compilation for up-to-date files results in mis-compilationPossibly taken @jespercockx claimed this 1 day ago. Openbug
Difficulty 3/5 1-2 days Newbie friendliness 52/100
agda/agda2hs#486 · 2 comments · 1 assignee ·
Maintainers usually reply within 1 day