1 files changed, 28 insertions, 0 deletions
diff --git a/lib/option.sail b/lib/option.sail
new file mode 100644
index 00000000..3869167b
--- /dev/null
+++ b/lib/option.sail
@@ -0,0 +1,28 @@
+$ifndef _OPTION
+$define _OPTION
+
+// The option type is treated specially by the lem backend, so it maps
+// onto the lem maybe type. If the constructors are named differently,
+// this won't work - also no other type should be created with
+// constructors named Some or None.
+
+union option ('a : Type) = {
+  Some : 'a,
+  None : unit
+}
+
+val is_none : forall ('a : Type). option('a) -> bool
+
+function is_none opt = match opt {
+  Some(_) => false,
+  None()  => true
+}
+
+val is_some : forall ('a : Type). option('a) -> bool
+
+function is_some opt = match opt {
+  Some(_) => true,
+  None()  => false
+}
+
+$endif