[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