[Agda] Data.Nat error

[Ruben Henner Zilibowitz]

Right. Thanks for that.

Now this (see bottom of transcript for error):

Ruben-Henner-Zilibowitzs-iMac:Agda rhz$ runghc Setup.hs configure

Setup.hs:2:0:
     Warning: Deprecated use of `defaultUserHooks'
              (imported from Distribution.Simple):
              Use simpleUserHooks or autoconfUserHooks, unless you  
need Cabal-1.2
              compatibility in which case you must stick with  
defaultUserHooks
Warning: defaultUserHooks in Setup script is deprecated.
Configuring Agda-2.1.3...
Ruben-Henner-Zilibowitzs-iMac:Agda rhz$ runghc Setup.hs build

Setup.hs:2:0:
     Warning: Deprecated use of `defaultUserHooks'
              (imported from Distribution.Simple):
              Use simpleUserHooks or autoconfUserHooks, unless you  
need Cabal-1.2
              compatibility in which case you must stick with  
defaultUserHooks
Preprocessing library Agda-2.1.3...
Building Agda-2.1.3...
[  1 of 175] Compiling Agda.Utils.Pointer ( src/full/Agda/Utils/ 
Pointer.hs, dist/build/Agda/Utils/Pointer.o )
[  2 of 175] Compiling Agda.Utils.Hash  ( src/full/Agda/Utils/Hash.hs,  
dist/build/Agda/Utils/Hash.o )
[  3 of 175] Compiling Agda.Utils.Trace ( src/full/Agda/Utils/ 
Trace.hs, dist/build/Agda/Utils/Trace.o )
[  4 of 175] Compiling Agda.Utils.Function ( src/full/Agda/Utils/ 
Function.hs, dist/build/Agda/Utils/Function.o )
[  5 of 175] Compiling Agda.Utils.Maybe ( src/full/Agda/Utils/ 
Maybe.hs, dist/build/Agda/Utils/Maybe.o )
[  6 of 175] Compiling Agda.Utils.Char  ( src/full/Agda/Utils/Char.hs,  
dist/build/Agda/Utils/Char.o )
[  7 of 175] Compiling Agda.Utils.ReadP ( src/full/Agda/Utils/ 
ReadP.hs, dist/build/Agda/Utils/ReadP.o )
[  8 of 175] Compiling Agda.Utils.Suffix ( src/full/Agda/Utils/ 
Suffix.hs, dist/build/Agda/Utils/Suffix.o )
[  9 of 175] Compiling Agda.Utils.Trie  ( src/full/Agda/Utils/Trie.hs,  
dist/build/Agda/Utils/Trie.o )
[ 10 of 175] Compiling Agda.Utils.QuickCheck ( src/full/Agda/Utils/ 
QuickCheck.hs, dist/build/Agda/Utils/QuickCheck.o )

src/full/Agda/Utils/QuickCheck.hs:21:0:
     Duplicate instance declarations:
       instance Applicative Gen
         -- Defined at src/full/Agda/Utils/QuickCheck.hs:(21,0)-(23,11)
       instance Applicative Gen -- Defined in Test.QuickCheck.Gen

Regards,

Ruben

On 09/11/2008, at 12:46 AM, Nils Anders Danielsson wrote:

> On 08/11/08 12:05, Ruben Henner Zilibowitz wrote:
>>
>> Unfortunately even after getting the latest patches form the Agda  
>> repository and rebuilding the error persists.
>
> Are you pulling from http://code.haskell.org/Agda?
>
> Ulf, can you add a permanent redirect from
> http://www.cs.chalmers.se/~ulfn/darcs/Agda2 to
> http://code.haskell.org/Agda? Or at least a message in
> _darcs/prefs/motd.
>
> -- 
> /NAD
>
> This message has been checked for viruses but the contents of an  
> attachment
> may still contain software viruses, which could damage your computer  
> system:
> you are advised to perform your own checks. Email communications  
> with the
> University of Nottingham may be monitored as permitted by UK  
> legislation.
>