[Agda] Duplicate binding for built-in thing
Shin-Cheng Mu
scm at iis.sinica.edu.tw
Thu Mar 6 04:28:34 CET 2008
Hi,
I don't know whether it is a bug or problem with my own
configuration. After pulling both the latest Agda implemenation
and the latest Standard Library, I got this error message
when I tried to load Data.Nat:
/Users/scm/Library/Agda2/lib/Data/Nat.agda:25,1-29
Duplicate binding for built-in thing NATURAL, previous binding to ℕ
when checking the pragma BUILTIN NATURAL ℕ
The same happens with other BUILTIN pragmas in Data.Nat
and Data.Bool.
If it matters... I have only set two directories in "Agda2
Include Dirs": the current directory, and the path to the
standard library.
Any ideas? Thanks you!
sincerely,
Shin
More information about the Agda
mailing list