[Agda] fast DecTotalOrder

[Andrea Vezzosi]

It seemed like you only wanted the decision procedure to be fast, not
the relation itself?

(2) _≤?_ to perform fast,

On Tue, Mar 24, 2015 at 2:30 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:
> 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
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda