		Search-engine friendly clone of the ACL2 documentation.

Rename-params

Rename one or more parameters in a function.

General Form:

(rename-params fn
               param-renaming
               &key
               :new-name      ; default :auto
               :verify-guards ; default :auto
               :guard-hints   ; default :auto
               :untranslate   ; default t
               :show-only     ; default nil
               :print         ; default :result
               )

Inputs:

fn — (required)

Function to transform

param-renaming — (required)

A doublet or list of doublets

:new-name — default :auto

New name to use for the function (if :auto, the transformation generates a name

:verify-guards — default :auto

Whether to verify guards of the new function(s).

:guard-hints — default :auto

Hints to use for the guard proof, or :auto, where :auto means to do the guard proof by appealing to the original function's guard obligation -- this can be slow).

:untranslate — default t

How to untranslate the function body after changing it.

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