Jesper Cockx

Unfortunately, Agda currently does not have any way to create a local shared closure: `let` bindings are inlined, while `where` declarations are lifted to the top level.

I was not the one who implemented it, but I believe `using` is desugared to an auxiliary function, so I'm afraid it's not really better performance-wise than a `where` declaration....

I'm not a Nix user so I'm afraid I'm not really able to provide any help here.

Alternatively we could use the following criterion for which functions are allowed to appear in compiled Haskell code: - has a `COMPILE AGDA2HS` pragma, - OR is a builtin function...

Could you explain how this would be different from the existing support for declaring agda2hs rewrite rules in a separate file? (see https://agda.github.io/agda2hs/features.html#rewrite-rules-and-prelude-imports) I think the idea here is solid,...

To support this properly we would need to have a dedicated pragma for indicating that an Agda postulate corresponds to an existing Haskell function, which we do not have at...

> To support this properly we would need to have a dedicated pragma for indicating that an Agda postulate corresponds to an existing Haskell function, which we do not have...

Since we already have a supported way to do this, I'm closing this issue.

I like the suggestion by @flupe , and I agree that we need test cases for rewrite rules.

This sounds like an upstream issue in Agda rather than a bug in agda2hs itself. Perhaps it could be fixed by https://github.com/agda/agda/pull/7251?