[Agda] duplicate builtin natural, succ, zero

[Nils Anders Danielsson]

On 2013-02-25 14:36, Peter Divianszky wrote:
> 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?

The BUILTIN machinery is not designed to accommodate multiple
definitions of a given BUILTIN. I'm not sure how hard it would be to
change things.

-- 
/NAD