1signature patriciaSyntax = 2sig 3 4 include Abbrev 5 6 val mk_ptree_type : hol_type -> hol_type 7 val dest_ptree_type : hol_type -> hol_type 8 val is_ptree_type : hol_type -> bool 9 10 val empty_tm : term 11 val leaf_tm : term 12 val branch_tm : term 13 val peek_tm : term 14 val find_tm : term 15 val add_tm : term 16 val add_list_tm : term 17 val remove_tm : term 18 val traverse_tm : term 19 val keys_tm : term 20 val transform_tm : term 21 val every_leaf_tm : term 22 val exists_leaf_tm : term 23 val size_tm : term 24 val depth_tm : term 25 val is_ptree_tm : term 26 val in_ptree_tm : term 27 val insert_ptree_tm : term 28 val branching_bit_tm : term 29 val ptree_of_numset_tm : term 30 val numset_of_ptree_tm : term 31 32 val mk_empty : hol_type -> term 33 val mk_leaf : term * term -> term 34 val mk_branch : term * term * term * term -> term 35 val mk_peek : term * term -> term 36 val mk_find : term * term -> term 37 val mk_add : term * term -> term 38 val mk_add_list : term * term -> term 39 val mk_remove : term * term -> term 40 val mk_traverse : term -> term 41 val mk_keys : term -> term 42 val mk_transform : term * term -> term 43 val mk_every_leaf : term * term -> term 44 val mk_exists_leaf : term * term -> term 45 val mk_size : term -> term 46 val mk_depth : term -> term 47 val mk_is_ptree : term -> term 48 val mk_in_ptree : term * term -> term 49 val mk_insert_ptree : term * term -> term 50 val mk_branching_bit : term * term -> term 51 val mk_ptree_of_numset : term * term -> term 52 val mk_numset_of_ptree : term -> term 53 54 val dest_leaf : term -> term * term 55 val dest_branch : term -> term * term * term * term 56 val dest_peek : term -> term * term 57 val dest_find : term -> term * term 58 val dest_add : term -> term * term 59 val dest_add_list : term -> term * term 60 val dest_remove : term -> term * term 61 val dest_traverse : term -> term 62 val dest_keys : term -> term 63 val dest_transform : term -> term * term 64 val dest_every_leaf : term -> term * term 65 val dest_exists_leaf : term -> term * term 66 val dest_size : term -> term 67 val dest_depth : term -> term 68 val dest_is_ptree : term -> term 69 val dest_in_ptree : term -> term * term 70 val dest_insert_ptree : term -> term * term 71 val dest_branching_bit : term -> term * term 72 val dest_ptree_of_numset : term -> term * term 73 val dest_numset_of_ptree : term -> term 74 75 val is_empty : term -> bool 76 val is_leaf : term -> bool 77 val is_branch : term -> bool 78 val is_peek : term -> bool 79 val is_find : term -> bool 80 val is_add : term -> bool 81 val is_add_list : term -> bool 82 val is_remove : term -> bool 83 val is_traverse : term -> bool 84 val is_keys : term -> bool 85 val is_transform : term -> bool 86 val is_every_leaf : term -> bool 87 val is_exists_leaf : term -> bool 88 val is_size : term -> bool 89 val is_depth : term -> bool 90 val is_is_ptree : term -> bool 91 val is_in_ptree : term -> bool 92 val is_insert_ptree : term -> bool 93 val is_branching_bit : term -> bool 94 val is_ptree_of_numset : term -> bool 95 val is_numset_of_ptree : term -> bool 96 97end 98