diff lib/ur/option.ur @ 961:8c37699de273

Grid sorting working
author Adam Chlipala <adamc@hcoop.net>
date Sat, 19 Sep 2009 13:32:33 -0400
parents da3ec6014d2f
children 757dbac0454d
line wrap: on
line diff
--- a/lib/ur/option.ur	Sat Sep 19 10:56:09 2009 -0400
+++ b/lib/ur/option.ur	Sat Sep 19 13:32:33 2009 -0400
@@ -7,6 +7,18 @@
                | (Some x, Some y) => x = y
                | _ => False)
 
+fun ord [a] (_ : ord a) =
+    mkOrd {Lt = fn x y =>
+                   case (x, y) of
+                       (None, Some _) => True
+                     | (Some x, Some y) => x < y
+                     | _ => False,
+           Le = fn x y =>
+                   case (x, y) of
+                       (None, _) => True
+                     | (Some x, Some y) => x <= y
+                     | _ => False}
+
 fun isNone [a] x =
     case x of
         None => True