[Agda] duplicate builtin natural, succ, zero

[Peter Divianszky]

By the way, why do not Agda have something like

     decimal_syntax N zero suc

instead of

     {-# BUILTIN NATURAL N    #-}
     {-# BUILTIN ZERO    zero #-}
     {-# BUILTIN SUC     suc  #-}

?

On 26/02/2013 07:46, Peter Divianszky wrote:
>
> 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
>>>
>>
>>
>