[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.
-------