Lines Matching refs:function
14 type function =
129 (* Split function definition *)
138 (* The function and theorem database *)
144 val get_translation_precise : hol_type -> hol_type -> (string,function) dict ref
145 val get_translation : hol_type -> hol_type -> (string,function) dict ref
157 val get_coding_function_precise : hol_type -> hol_type -> string -> function
158 val get_coding_function : hol_type -> hol_type -> string -> function
165 val add_coding_function_precise : hol_type -> hol_type -> string -> function -> unit
166 val add_coding_function : hol_type -> hol_type -> string -> function -> unit
169 val get_source_function_precise : hol_type -> string -> function
170 val get_source_function : hol_type -> string -> function
177 val add_source_function_precise : hol_type -> string -> function -> unit
178 val add_source_function : hol_type -> string -> function -> unit
203 (* Removal of function splits *)
214 (* Full function creation *)
220 val add_coding_function_generator : hol_type -> string -> (hol_type -> bool) -> (hol_type -> function) -> unit
221 val add_source_function_generator : string -> (hol_type -> bool) -> (hol_type -> function) -> unit