stdlib/option.mlw

   1 (** {1 Option type} *)
   2
   3 module Option
   4
   5   type option 'a = None | Some 'a
   6
   7   let predicate is_none (o: option 'a)
   8     ensures { result <-> o = None }
   9   = match o with None -> true | Some _ -> false end
  10
  11 end
  12
  13 module Map
  14
  15   use Option
  16
  17   function map (f: 'a -> 'b) (o: option 'a) : option 'b
  18   = match o with None -> None | Some x -> Some (f x) end
  19
  20 end