comparison 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
comparison
equal deleted inserted replaced
960:6f34950825b6 961:8c37699de273
4 mkEq (fn x y => 4 mkEq (fn x y =>
5 case (x, y) of 5 case (x, y) of
6 (None, None) => True 6 (None, None) => True
7 | (Some x, Some y) => x = y 7 | (Some x, Some y) => x = y
8 | _ => False) 8 | _ => False)
9
10 fun ord [a] (_ : ord a) =
11 mkOrd {Lt = fn x y =>
12 case (x, y) of
13 (None, Some _) => True
14 | (Some x, Some y) => x < y
15 | _ => False,
16 Le = fn x y =>
17 case (x, y) of
18 (None, _) => True
19 | (Some x, Some y) => x <= y
20 | _ => False}
9 21
10 fun isNone [a] x = 22 fun isNone [a] x =
11 case x of 23 case x of
12 None => True 24 None => True
13 | Some _ => False 25 | Some _ => False