diff options
Diffstat (limited to 'src/option_key_fn.sml')
-rw-r--r-- | src/option_key_fn.sml | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/option_key_fn.sml b/src/option_key_fn.sml new file mode 100644 index 00000000..ba636d4e --- /dev/null +++ b/src/option_key_fn.sml @@ -0,0 +1,11 @@ +functor OptionKeyFn(K : ORD_KEY) : ORD_KEY = 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 |