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
_______________________________________________
Ur mailing list
[email protected]
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
