diff options
Diffstat (limited to 'src/option_key_fn.sml')
-rw-r--r-- | src/option_key_fn.sml | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/option_key_fn.sml b/src/option_key_fn.sml new file mode 100644 index 00000000..27ba9138 --- /dev/null +++ b/src/option_key_fn.sml @@ -0,0 +1,12 @@ +functor OptionKeyFn(K : ORD_KEY) + : ORD_KEY where type ord_key = K.ord_key option = struct + +type ord_key = K.ord_key option + +val compare = + fn (NONE, NONE) => EQUAL + | (NONE, _) => LESS + | (_, NONE) => GREATER + | (SOME x, SOME y) => K.compare (x, y) + +end |