[Agda] irrelevant fields and EqReasoning

Jean-Philippe Bernardy bernardy at chalmers.se
Fri Jul 20 14:57:23 CEST 2012

> > I think that you can use a "syntax" declaration to swap the order of
> > arguments even when there is a dependency.
> Glory to the people!


> But two questions:
> 1. Can you attach precedences to syntax declarations?

Last time I looked at the code, the fixity was inherited from the
identifier that the syntax declaration "aliases".

>  (Or perhaps the
> higher-level question, how are syntax declarations supposed to
> interact with infix/mixfix operators? Are they meant to replace them?)

There is no plan like this.

> 2. How do syntax declarations get exported from a module? Can you
> hide/rename them?

Not as far as I know.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120720/fd473b69/attachment.html

More information about the Agda mailing list