summaryrefslogtreecommitdiff
path: root/src/option_key_fn.sml
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@mit.edu>2015-12-23 16:01:51 -0500
committerGravatar Benjamin Barenblat <bbaren@mit.edu>2015-12-23 16:01:51 -0500
commit3d3886672433f0775f772d8d2ee47c5f5e0bc745 (patch)
tree072d171c17d92a6696024256c4b2f5aaa760df35 /src/option_key_fn.sml
parentbf037ce78c2c76a34ecca0fb8bafa5d5be38968a (diff)
parent4be7962adf740a35222bfd99608c04329a802a04 (diff)
Merge branch 'upstream' into dfsg_clean20151220+dfsg
Diffstat (limited to 'src/option_key_fn.sml')
-rw-r--r--src/option_key_fn.sml12
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