[Agda] fast DecTotalOrder

[Sergei Meshveliani]

On Tue, 2015-03-24 at 14:05 +0100, Nils Anders Danielsson wrote:
> 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 _≡_ _<_
> 


This looks like a pitfall.
Probably, there are many applications which use a generic
StrictTotalOrder._<_.
And as soon as  A = Bin  is substituted, their performance cost will
explode unexpectedly.   

Regards,

------
Sergei