1signature optionSyntax =
2sig
3  include Abbrev
4
5  val mk_option        : hol_type -> hol_type
6  val dest_option      : hol_type -> hol_type
7  val is_option        : hol_type -> bool
8
9  val none_tm          : term
10  val some_tm          : term
11  val the_tm           : term
12  val option_map_tm    : term
13  val option_join_tm   : term
14  val is_some_tm       : term
15  val is_none_tm       : term
16  val option_case_tm   : term
17
18  val mk_none          : hol_type -> term
19  val mk_some          : term -> term
20  val mk_the           : term -> term
21  val mk_option_map    : term * term -> term
22  val mk_option_join   : term -> term
23  val mk_is_some       : term -> term
24  val mk_is_none       : term -> term
25  val mk_option_case   : term * term * term -> term
26
27  val dest_none        : term -> hol_type
28  val dest_some        : term -> term
29  val dest_the         : term -> term
30  val dest_option_map  : term -> term * term
31  val dest_option_join : term -> term
32  val dest_is_some     : term -> term
33  val dest_is_none     : term -> term
34  val dest_option_case : term -> term * term * term
35
36  val is_none          : term -> bool
37  val is_some          : term -> bool
38  val is_the           : term -> bool
39  val is_option_map    : term -> bool
40  val is_option_join   : term -> bool
41  val is_is_some       : term -> bool
42  val is_is_none       : term -> bool
43  val is_option_case   : term -> bool
44
45  val lift_option      : hol_type -> ('a -> term ) -> 'a option -> term
46end
47