[Agda] broken

Ruben Henner Zilibowitz rzilibowitz at yahoo.com.au
Sat Jul 19 06:58:22 CEST 2008


I've just pulled the most recent patches for agda and its associated  
repositories. However now it doesn't work. I am pretty sure it worked  
before I pulled the darcs patches. Any help would be appreciated thanks.

Here is what I'm getting:

agda -I -i AFP08/Library/ Test.agda
                  _        ______
    ____         | |      |_ __ _|
   / __ \        | |       | || |
  | |__| |___  __| | ___   | || |
  |  __  / _ \/ _  |/ __\  | || |   Agda 2 Interactive
  | |  |/ /_\ \/_| / /_| \ | || |
  |_|  |\___  /____\_____/|______|  Type :? for help.
         __/ /
         \__/
Checking Data.Nat ( /Users/rhz/Documents/dev/Agda/AFP08/Library/Data/ 
Nat.agda )
Checking Data.Bool ( /Users/rhz/Documents/dev/Agda/AFP08/Library/Data/ 
Bool.agda )
Skipping Logic.Base ( /Users/rhz/Documents/dev/Agda/AFP08/Library/ 
Logic/Base.agdai )
Skipping Logic.Id ( /Users/rhz/Documents/dev/Agda/AFP08/Library/Logic/ 
Id.agdai )
/Users/rhz/Documents/dev/Agda/AFP08/Library/Data/Bool.agda:15,1-43
Panic: Mismatch in number of constructors
when checking the pragma COMPILED_DATA Bool Bool True False
Failed.
Main> :q

The file Test.agda contains:

module Test where

open import Data.Nat

Regards,

Ruben



More information about the Agda mailing list