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