Mercurial > urweb
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