Lines Matching refs:list
50 val type_vars_avoiding_itself : term -> hol_type -> hol_type list
52 val get_sub_types : hol_type -> hol_type -> hol_type list
83 val encode_decode_map_tactic : hol_type -> hol_type -> term list * term ->
84 (term list * term) list * (thm list -> thm)
85 val encode_map_encode_tactic : hol_type -> hol_type -> term list * term ->
86 (term list * term) list * (thm list -> thm)
87 val map_compose_tactic : hol_type -> term list * term -> (term list * term) list * (thm list -> thm)
88 val encode_detect_all_tactic : hol_type -> hol_type -> term list * term ->
89 (term list * term) list * (thm list -> thm)
91 val decode_encode_fix_tactic : hol_type -> 'a -> term list * term ->
92 (term list * term) list * (thm list -> thm)
93 val fix_id_tactic : hol_type -> hol_type -> term list * term ->
94 (term list * term) list * (thm list -> thm)
95 val general_detect_tactic : hol_type -> hol_type -> term list * term ->
96 (term list * term) list * (thm list -> thm)
98 val all_id_tactic : 'a -> term list * term -> (term list * term) list * (thm list -> thm)
99 val map_id_tactic : 'a -> term list * term -> (term list * term) list * (thm list -> thm)
104 val mk_destructors : hol_type -> hol_type -> (thm list * thm list)