[Agda] fast DecTotalOrder

[Sergei Meshveliani]

On Tue, 2015-03-24 at 11:48 +0100, Nils Anders Danielsson wrote:
> On 2015-03-24 11:29, Sergei Meshveliani wrote:
> > First I thought of  Bin,  but then discovered that  _<_  is done there
> > by conversion to  Nat,  which is very expensive.
> > Right?
> 
> The predicate _<_ is defined using the corresponding predicate for
> natural numbers. However, the compare function compares bits.
> 


So,  Data.Bin.StrictTotalOrder.compare  costs  
O(bit length of arguments).
Right?

And as `compare' is O(bit length) for Bin, why does not Standard library
implement _<_ for Bin via `compare' ?

And then, how to define fast _≤_ for Bin ?
I see
   _≤_ : Rel Bin _
   x ≤ y  with compare x y
   ...    | tri< x<y _ _ = ⊤
   ...    | tri≈ _   _ _ = ⊤
   ...    | tri> _   _ _ = ⊥,

and see proofs for  Decidable  and  reflexivity  for _≤_.
But this definition somehow does no look nice: it looses the witnesses
provided from `compare'.

Thanks,

------
Sergei