[Ur] ord class and performance

[Adam Chlipala]

Yes, that's the sort of patch I meant to say I was happy to accept. :)

On 03/05/2015 10:45 PM, Timothy Beyer wrote:
> At Thu, 05 Mar 2015 15:07:29 -0500,
> Adam Chlipala wrote:
>> I'd consider accepting a patch making this change.  In practice, though,
>> it probably doesn't make a noticeable performance difference in most cases.
>>
> Would it be possible for Ur/Web to include a compare operation, or is it already available?
>
> Currently, I use the following in my code, which I loosely modeled after the Haskell compare function:
>
> datatype ordering = Eq | Gt | Lt
> fun compare [a] (_: ord a) (_: eq a) (x: a) (y: a) : ordering =
>    if x = y then Eq else if x > y then Gt else Lt
>
> Does this make sense, or is it not general enough to use in the basis?
>
> Regards,
> Tim