[Agda] Duplicate binding for built-in thing

[Ulf Norell]

On Thu, Mar 6, 2008 at 4:28 AM, Shin-Cheng Mu <scm at iis.sinica.edu.tw> wrote:

> 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.


This rings a bell. I think it's a bug. It should go away if you remove all
interface (.agdai) files.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080306/3c0f49a9/attachment.html