[Agda] numeric literals

[Sergei Meshveliani]

People,

I have a certain library for Bin which uses exclusively naive unary Nat
arithmetic. To arrange this, I copy Data.Nat.Base to my root directory
as Nat.agda,
also copy there .../lib/prim/Agda/Builtin/Nat.agda,
with removing the BUILTIN pragma,
and removed various unneeded items from both.
Also copied there Data.Nat.Properties as NatProp.
And changed everywhere the import to Nat and NatProp.

After this, Agda does not understand the literals 0 and 1 in the code in
this Bin3 library, so that I need to write zero and (suc zero)
respectively.
Can anybody, please, explain, how does this occur that numeric literals
are lost?
How to return them?

Thanks,

------
Sergei

[Nils Anders Danielsson]

Post by Sergei Meshveliani
Can anybody, please, explain, how does this occur that numeric literals
are lost?
How to return them?

http://agda.readthedocs.io/en/v2.5.3/language/literal-overloading.html