[Agda] fast DecTotalOrder

[Nils Anders Danielsson]

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

Why? Do you plan to evaluate the proofs? Or do you worry about the space
consumed by unevaluated thunks?

-- 
/NAD