1signature HolKernelDoc = 2sig 3 (* This signature file is for documentation purposes only *) 4 5 type term = Term.term 6 type hol_type = Type.hol_type 7 type 'a set = 'a HOLset.set 8 type ('a,'b) subst = ('a,'b) Lib.subst 9 10 val gen_find_term: (term list * term -> 'a option) -> term -> 'a option 11 val gen_find_terms: (term list * term -> 'a option) -> term -> 'a list 12 val bvk_find_term: 13 (term list * term -> bool) -> (term -> 'a) -> term -> 'a option 14 val dest_binder: term -> exn -> term -> term * term 15 val dest_binop: term -> exn -> term -> term * term 16 val dest_monop: term -> exn -> term -> term 17 val dest_quadop: term -> exn -> term -> term * term * term * term 18 val dest_triop: term -> exn -> term -> term * term * term 19 val disch: term * term list -> term list 20 val find_maximal_terms: (term -> bool) -> term -> term set 21 val find_term: (term -> bool) -> term -> term 22 val find_terms: (term -> bool) -> term -> term list 23 val ho_match_term0: 24 hol_type list -> term set -> term -> term -> 25 {redex: term, residue: int} list * 26 {redex: term, residue: term} list * 27 ((hol_type, hol_type) subst * hol_type list) 28 val ho_match_term: 29 hol_type list -> term set -> term -> term -> 30 {redex: term, residue: term} list * (hol_type, hol_type) subst 31 val list_mk_fun: hol_type list * hol_type -> hol_type 32 val list_mk_icomb: term -> term list -> term 33 val list_mk_lbinop: ('a -> 'a -> 'a) -> 'a list -> 'a 34 val list_mk_rbinop: ('a -> 'a -> 'a) -> 'a list -> 'a 35 val lspine_binop: ('a -> ('a * 'a) option) -> 'a -> 'a list 36 val mk_binder: term -> string -> term * term -> term 37 val mk_binop: term -> term * term -> term 38 val mk_monop: term -> term -> term 39 val mk_quadop: term -> term * term * term * term -> term 40 val mk_triop: term -> term * term * term -> term 41 val sdest_binder: string * string -> exn -> term -> term * term 42 val sdest_binop: string * string -> exn -> term -> term * term 43 val sdest_monop: string * string -> exn -> term -> term 44 val spine_binop: ('a -> ('a * 'a) option) -> 'a -> 'a list 45 val strip_binop: ('a -> ('a * 'a) option) -> 'a -> 'a list 46 val strip_comb: term -> term * term list 47 val strip_fun: hol_type -> hol_type list * hol_type 48 val strip_gen_right_opt: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list 49 val strip_gen_right: ('a -> 'a * 'b) -> 'a -> 'a * 'b list 50 val strip_gen_left_opt: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a 51 val strip_gen_left: ('a -> 'b * 'a) -> 'a -> 'b list * 'a 52 val sort_vars: string list -> term list -> term list 53 val subst_occs: 54 int list list -> {redex: term, residue: term} list -> term -> term 55 val syntax_fns: 56 {n: int, make: term -> 'a -> term, dest: term -> exn -> term -> 'b} -> 57 string -> string -> term * ('a -> term) * (term -> 'b) * (term -> bool) 58 val syntax_fns1: 59 string -> string -> term * (term -> term) * (term -> term) * (term -> bool) 60 val syntax_fns2: 61 string -> string -> 62 term * (term * term -> term) * (term -> term * term) * (term -> bool) 63 val syntax_fns3: 64 string -> string -> 65 term * (term * term * term -> term) * (term -> term * term * term) * (term -> bool) 66 val syntax_fns4: 67 string -> string -> 68 term * (term * term * term * term -> term) * (term -> term * term * term * term) * (term -> bool) 69 val term_size: term -> int 70 71end 72