[Agda] irrelevant fields and EqReasoning

[Jean-Philippe Bernardy]

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

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