Lines Matching refs:list
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
13 (term list * term -> bool) -> (term -> 'a) -> term -> 'a option
19 val disch: term * term list -> term list
22 val find_terms: (term -> bool) -> term -> term list
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)
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
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
54 int list list -> {redex: term, residue: term} list -> term -> term