[Agda] blowUpSparseVec error

Andreas Abel andreas.abel at ifi.lmu.de
Mon Mar 18 13:15:16 CET 2013


Start here:

   http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Download

You will need darcs to clone the dev repo and ghc>7.0 to compile.
Cheers,
Andreas

On 18.03.13 11:58 AM, Darryl McAdams wrote:
> I only have what 'cabal install agda' installs. How would I install the
> dev version?
> - darryl
>
> ------------------------------------------------------------------------
> *From:* Nils Anders Danielsson <nad at chalmers.se>
> *To:* Darryl McAdams <psygnisfive at yahoo.com>
> *Cc:* Agda List <agda at lists.chalmers.se>
> *Sent:* Monday, March 18, 2013 6:15 AM
> *Subject:* Re: [Agda] blowUpSparseVec error
>
> 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
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/


More information about the Agda mailing list