Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Compiling declared but not-yet-defined datatype silently generates no code #346

Open
jespercockx opened this issue Jul 27, 2024 · 0 comments
Open

Compiling declared but not-yet-defined datatype silently generates no code #346

jespercockx opened this issue Jul 27, 2024 · 0 comments
Labels
bug Something isn't working
Milestone
1.4

Comments

@jespercockx
Copy link
Member

Minimal example:

data D : Set
{-# COMPILE AGDA2HS D #-}
data D where  C : D

This generates an empty Haskell file. It should either raise an error, or just compile the actual definition.
@jespercockx jespercockx added the bug Something isn't working label Jul 27, 2024
jespercockx added a commit to jespercockx/agda-core that referenced this issue Jul 27, 2024
@jespercockx
Work around for agda/agda2hs#346
11bbc77
@jespercockx jespercockx added this to the 1.4 milestone Oct 31, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug Something isn't working
Projects
None yet
Milestone
1.4
Development

No branches or pull requests
1 participant
@jespercockx