[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