[Agda] duplicate builtin natural, succ, zero

[Peter Divianszky]

A short testcase is three separate files:

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ X.agda
module X where

data N : Set where
   zero : N
   suc : N -> N

{-# BUILTIN NATURAL N    #-}
{-# BUILTIN ZERO    zero #-}
{-# BUILTIN SUC     suc  #-}
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ end of X.agda

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Y.agda
module Y where

data N : Set where
   zero : N
   suc : N -> N

{-# BUILTIN NATURAL N    #-}
{-# BUILTIN ZERO    zero #-}
{-# BUILTIN SUC     suc  #-}
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ end of Y.agda

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Z.agda
module Z where

import X
import Y

x = X.zero
y = Y.zero
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ end of Z.agda

which doesn't compile.


On 25/02/2013 15:05, Andreas Abel wrote:
> You mean builtins are not subject to import/export, like instances in
> Haskell?
>
> What would be a short test case for your problem?
>
> Cheers,
> Andreas
>
> On 25.02.2013 14:36, Peter Divianszky wrote:
>>
>> Hi,
>>
>> Agda does not allow duplicate builtin bindings to natural numbers
>>
>> {-# BUILTIN NATURAL ℕ    #-}
>> {-# BUILTIN ZERO    zero #-}
>> {-# BUILTIN SUC     suc  #-}
>>
>> even if the bindings are in different modules which does not depend on
>> each-other.
>>
>> This makes hard to use the Standard Libraries with other developments
>> (for example the tutorial I'm working on).
>>
>> How hard would be to fix this?
>>
>> Peter
>>
>>
>> Duplicate binding for built-in thing NATURAL, previous binding to
>> .Data.Nat.ℕ
>> when checking the pragma BUILTIN NATURAL ℕ
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
>