[Agda] fast DecTotalOrder

Nils Anders Danielsson nad at cse.gu.se
Tue Mar 24 11:48:38 CET 2015


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.

-- 
/NAD


More information about the Agda mailing list