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