		Search-engine friendly clone of the ACL2 documentation.

Copy-function

Make a copy of a function, with recursive calls appropriately renamed.

General Form:

(copy-function fn
               &key
               :show-only          ; default nil
               :print              ; default :result
               :new-name           ; default :auto
               :theorem-disabled   ; default nil
               :function-disabled  ; default :auto
               :verify-guards      ; default :auto
               :guard-hints        ; default :auto
               :measure            ; default :auto
               :measure-hints      ; default :auto
               :normalize          ; default t
               )

Inputs:

fn — (required)

The name of the function to transform.

:show-only — default nil

Whether to simply show the result, not create it.

:print — default :result

How much detail to print.

:new-name — default :auto

The name of the new function to be created.

:theorem-disabled — default nil

Whether to disable the 'becomes theorem'.

:function-disabled — default :auto

Whether to disable the new function.

:verify-guards — default :auto

Whether to verify the guards of the new function.

:guard-hints — default :auto

Hints to use for the guard proof.

:measure — default :auto

Measure to use for the new function.

:measure-hints — default :auto

Hints to use for the measure/termination proof.

:normalize — default t

Whether to normalize the new function body, as ACL2 usually does.

Description:

To inspect the resulting forms, call show-copy-function on the same arguments.