[Agda-dev] Clauses and trailing implicit arguments

Philipp Hausmann p.hausmann at students.uu.nl
Fri Jan 23 14:30:51 CET 2015


Is reported:
https://code.google.com/p/agda/issues/detail?id=1412

Btw, you can also find the examples mentioned in the issue in my github 
repo:
https://github.com/phile314/agda-compiler-tests

This is a work-in-progress, so it's a bit tricky to run the tests right 
now, but I intend
to fix that in the coming weeks. That should give us some tests for at 
least the MAlonzo (and my own) backend.

Philipp

On 01/23/2015 12:36 PM, Andrés Sicard-Ramírez wrote:
>
> On 19 January 2015 at 19:39, Philipp Hausmann 
> <p.hausmann at students.uu.nl <mailto:p.hausmann at students.uu.nl>> wrote:
>
>     I have a question about the internal Clauses/CompiledClauses
>     representation of Agda. I just learned that for certain corner-cases,
>     different clauses of the same function may take a different number
>     of arguments. This seems to break the Epic (and my own new) backend;
>
>
> ​ Using a minimal example, could you report the Epic issue in 
> https://code.google.com/p/agda/issues/list, please.
>
> Thanks,
>
> -- 
> Andrés

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


More information about the Agda-dev mailing list