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 _≡_ _<_ -- /NAD