[Agda] irrelevant fields and EqReasoning

Nils Anders Danielsson nad at chalmers.se
Wed Aug 8 10:27:33 CEST 2012

On 2012-07-20 14:57, Jean-Philippe Bernardy wrote:
>     2. How do syntax declarations get exported from a module? Can you
>     hide/rename them?
> Not as far as I know.

You can hide them by hiding the underlying name. You can't rename them.


More information about the Agda mailing list