[Agda] Duplicate binding for built-in thing

Shin-Cheng Mu scm at iis.sinica.edu.tw
Fri Mar 7 02:59:01 CET 2008


On Thu, 6 Mar 2008 11:51, Ulf Norell <ulfn at cs.chalmers.se> wrote:
> This rings a bell. I think it's a bug. It should go away if you  
> remove all
> interface (.agdai) files.

Yes, the problem went away after I remove all the .agdai
files. Thanks!



More information about the Agda mailing list