[Agda] Binary-4 announcement

[Sergei Meshveliani]

Announcement
------------

Binary-4 -- a Pure Binary Natural Number Arithmetic library for Agda

is available on

http://www.botik.ru/pub/local/Mechveliani/binNat/4/
ftp://ftp.botik.ru/pub/local/Mechveliani/binNat/4/

(see announcement.txt).

Changes in Binary-4 with respect to Binary-3.2
----------------------------------------------

* It has simpler proofs and simpler algorithms,

* It has a faster divMod operation in the case of small divisor values
(this matter has been pointed out by Arseniy Alekseyev).

* It is used a different representation for Bin:
data Bin : Set
where
0# : Bin
2suc : Bin -> Bin -- \n-> 2*(1+n) arbitrary nonzero even
suc2* : Bin -> Bin -- \n-> 1 + 2n arbitrary odd

* _<_ on Bin is defined defined by mapping to Nat
(similar as in Standard library).


Thanks. I am grateful to Arseniy Alekseyev for his notes and help.
-------