mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
21 lines
351 B
Plaintext
21 lines
351 B
Plaintext
(** {1 Option type} *)
|
|
|
|
module Option
|
|
|
|
type option 'a = None | Some 'a
|
|
|
|
let predicate is_none (o: option 'a)
|
|
ensures { result <-> o = None }
|
|
= match o with None -> true | Some _ -> false end
|
|
|
|
end
|
|
|
|
module Map
|
|
|
|
use Option
|
|
|
|
function map (f: 'a -> 'b) (o: option 'a) : option 'b
|
|
= match o with None -> None | Some x -> Some (f x) end
|
|
|
|
end
|