[Agda] duplicate builtin natural, succ, zero

[Andreas Abel]

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
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/