acl2/ml/acl2encodeLib.sig

5 (*    should be used in order of definition. Eg, if the function f calls the *)
6 (*    function g, then g should be translated before f. Additionally, if     *)
7 (*    f takes as argument a type t, then a 'recognition' function must be    *)
8 (*    generated for t before it can be used. The function,                   *)
16 (*        Missing rewrite: A function that is relied upon by the function    *)
19 (*           missing function, or flattening the recognizer for the required *)
20 (*           type. If the function may not be translated automatically,      *)
44 (*    For a recursive function we must therefore prove two theorem forms.    *)
53 (*    found by using the function:                                           *)
83 (*    This function can be used before or after initialise_type is called.   *)
104 (*    process, for more information see the function definition itself and   *)
105 (*    the function encodeLib.encode_type.                                    *)
108 (*    This function should be used to encode types added via hol_datatype.   *)
129 (*    Each function takes an associative list, mapping function constants to *)
130 (*    names for the translated function. For example:                        *)
132 (*    Lists are used throughout to support mutually recursive function       *)
143 (*        The second argument to this function is then a list of helper      *)
151 (*    The final function should be used for definitions which are under      *)
153 (*    under which the function may be translated, eg:                        *)
174 (*     for each mutually recursive function involved.                        *)
176 (*     For a simple, or conditional, function, only the following form of    *)
184 (*     In the case of a limited function, eg. LAST, the fusion theorem can   *)
194 (*     function for a ground type (eg. num).                                 *)
213 (*    to represent the encoded function, and a function defined to match it  *)
219 (*    sexp that demonstrates that the function terminates. The tactic:       *)
249 (*     Both functions require a 'naming' function to produce names for       *)