[Agda] irrelevant fields and EqReasoning

Jean-Philippe Bernardy bernardy at chalmers.se
Thu Jul 19 22:01:51 CEST 2012

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

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

More information about the Agda mailing list