[Agda] duplicate builtin natural, succ, zero

[Peter Divianszky]

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 ℕ