		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
               :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
               :show-only         ; default nil
               :print             ; default :result
               )

Inputs:

fn — (required)

The name of the function to transform.

: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.

:show-only — default nil

Whether to simply show the result, without actually creating it.

:print — default :result

How much detail to print, an apt::print-specifier.

Description:

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