[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.

-- 
/NAD


More information about the Agda mailing list