[Agda] () is not a valid expression

[J.Burton at brighton.ac.uk]

> From: Nils Anders Danielsson [mailto:nad at Cs.Nott.AC.UK]
> Sent: Tue 11/18/2008 11:23 PM
> To: Burton James
> Cc: agda at lists.chalmers.se
> Subject: Re: [Agda] () is not a valid expression
> 
[..]
> If you used Agda in batch mode, did you rebuild the batch mode tool in
> src/main? (Cabal does not handle a library and an executable in the same
> package very well, hence the current setup.) If that was not the problem
> I would double-check that I was actually using the latest version of
> Agda.

Hi Nils,

I was using emacs and AFAIK I must be using the latest version, although I suppose I must be doing something strange. Here's me repeating the process of updating it:

jim at daisy:~/agda/Agda$ darcs pull
Pulling from "http://code.haskell.org/Agda"...
No remote changes to pull in!
jim at daisy:~/agda/Agda$ cabal install
Resolving dependencies...
Configuring Agda-2.1.3...
Preprocessing library Agda-2.1.3...
Building Agda-2.1.3...
/usr/bin/ar: creating dist/build/libHSAgda-2.1.3.a
Installing library in /home/jim/.cabal/lib/Agda-2.1.3/ghc-6.8.2
Registering Agda-2.1.3...
Reading package info from "dist/installed-pkg-config" ... done.
Saving old package config file... done.
Writing new package config file... done.

jim at daisy:~/agda/Agda$ cd ../lib/
jim at daisy:~/agda/lib$ darcs pull
Pulling from "http://www.cs.nott.ac.uk/~nad/repos/lib"...
No remote changes to pull in!

And emacs-mode gives me the error about (). If I rebuild in src/main and try there I get the same thing:

jim at daisy:~/agda/lib$ agda --compile Data/Bool.agda
Skipping Data.Function ( /home/jim/agda/lib/Data/Function.agdai )
[..]
/home/jim/agda/lib/Data/Bool.agda:65,25-27
() is not a valid expression.
when scope checking ()

-----------------

Jim
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20081119/14ded64c/attachment-0001.html