[Agda] numeric literals

Sergei Meshveliani mechvel at botik.ru
Wed Dec 20 17:27:28 CET 2017


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





More information about the Agda mailing list