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