Merge branch 'lima' into master

2020-10-13 10:22:05 +02:00
parent 079b3a45c9 25fa365c29
commit ac673602b9
16 changed files with 193 additions and 96 deletions
@@ -22,7 +22,11 @@ namespace Option =

 /** Assume it is `Some`
 */
-  function force(o : option('a)) : 'a = default(abort("Forced None value"), o)
+  function force(o : option('a)) : 'a = switch(o)
+    None    => abort("Forced None value")
+    Some(x) => x
+
+  function contains(e : 'a, o : option('a)) = o == Some(e)

  function on_elem(o : option('a), f : 'a => unit) : unit = match((), f, o)