[Agda] fast DecTotalOrder

[Sergei Meshveliani]

On Tue, 2015-03-24 at 16:00 +0100, Nils Anders Danielsson wrote:
> 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?
> 

Sorry, I have forgotten that in my example,  _<_  and  _≤?_  are used
differently.
Probably, _<_ and _≤_ are only for proofs.

A false alarm.

In my example, it is essential that the second part for the proof for
`sort' is not evaluated (unless the performance cost explodes).

Sometimes it may be good to evaluate a proof. But probably I would not
rely in such a case that _<_ is fast.  Otherwise it would be generally
too difficult to set proofs.

Regards,

------
Sergei