[Ur] ord class and performance

[Adam Chlipala]

I'd consider accepting a patch making this change.  In practice, though, 
it probably doesn't make a noticeable performance difference in most cases.

On 02/27/2015 10:21 AM, Gabriel Riba wrote:
> When I make a lookup in a "Binary Search Tree" to decide whether it is 
> equal to the root payload or it is in the left or right branch,
>
> given the actual ord class definition, I have to make the comparison 
> twice: with "lt" and "le", or with the help of the eq class, "eq" and 
> then "lt".
>
> while a "compare" function giving a ternary result {-1,0,1} or {LT, 
> EQ, GT} (haskell style) would cut the comparisons in half.
>
> A possible solution would be to substitute in the constructor function 
> mkOrd, the second function "le" with a ternary result "compare" 
> function, and define "le" in terms of "compare".