[Agda] irrelevant fields and EqReasoning

[Noam Zeilberger]

On Thu, Jul 19, 2012 at 10:01 PM, Jean-Philippe Bernardy
<bernardy at chalmers.se> wrote:
>>
>> Time to liberate dependent types from the shackles of left-to-right
>> scoping!
>>
>
> 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?  (Or perhaps the
higher-level question, how are syntax declarations supposed to
interact with infix/mixfix operators? Are they meant to replace them?)

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

Noam