[Agda] blowUpSparseVec error

Nils Anders Danielsson nad at chalmers.se
Mon Mar 18 11:15:42 CET 2013


On 2013-03-18 09:42, Darryl McAdams wrote:
> http://hpaste.org/84240
>
> yields the error
>
> blowUpSparseVec (n = 2) aux i=3 j=3 length l = 2
>
> when the holes on the last few lines are given the values inside the {! !}
>
> This is with the most recent install of agda. Is there any fix to this?

This looks related to some recently reported bugs:

   http://code.google.com/p/agda/issues/detail?id=754
   http://code.google.com/p/agda/issues/detail?id=787

Do you have the most recent development version?

-- 
/NAD


More information about the Agda mailing list