Lucas Escot

> I think that we should just deprecate the polarity pragmas once this pr is merged. I have to emphasize the following explanation at the top of the PR: >...

Thank you for your work! However I don't think it is the right solution _for this specific issue_ just yet. The thing is, because the document metadata is accessible from...

Let me reformulate. I have no doubt your PR is useful and would love to see it merged. What I'm arguing is that it does not resolve **this** issue, hence...

Closing this now. After @ip1981's comment and PR more than a week ago I started investigating whether it could be used as a starting point for solving this issue. Still,...

That's also what we used in agda-core! https://github.com/jespercockx/agda-core/blob/2229d9ec6b78448b93b492b681a38a62f6efe121/src/Agda/Core/Typing.agda#L69

May I suggest having a cursed syntax: ```agda infixr 5 Let syntax Let a (λ x → b) = let[ x ← a ] b t : Bool t =...

Note: Haskell's let bindings are *always* recursive, so we should make sure that the name used in the `Let` does not appear in the expression being bound to prevent incorrect...

I think agda2hs should definitely allow rewrite rules to constructors! Though personally I would refrain from adding more fields to rewrite rules in the config file. Perhaps we could make...

If we want to stay faithful to [the Haskell interface](https://hackage.haskell.org/package/base-4.20.0.0/docs/Data-Eq.html), shouldn't `_/= _` be turned into a record field instead?

In [this paper](https://arxiv.org/abs/2205.08718), they define some Agda operators to mimic plain Haskell guards, maybe we could get some inspiration from this and do the reverse transformation from Agda to Haskell?...