[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