[Ur] ord class and performance

[Timothy Beyer]

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