[Agda] duplicate builtin natural, succ, zero

Nils Anders Danielsson nad at chalmers.se
Tue Feb 26 11:08:29 CET 2013

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.


More information about the Agda mailing list