[Agda] irrelevant fields and EqReasoning

[Jean-Philippe Bernardy]

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

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