[Agda] fast DecTotalOrder

Nils Anders Danielsson nad at cse.gu.se
Tue Mar 24 14:05:10 CET 2015


On 2015-03-24 13:51, Sergei Meshveliani wrote:
> And as `compare' is O(bit length) for Bin, why does not Standard library
> implement _<_ for Bin via `compare' ?

_<_ is used in the specification of compare:

   _<_     : Bin → Bin → Set
   compare : Trichotomous _≡_ _<_

-- 
/NAD



More information about the Agda mailing list