		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
               :show-only      ; default nil
               :print          ; default :result
               :new-name       ; default :auto
               :verify-guards  ; default :auto
               :untranslate    ; default t
               )

Inputs:

fn — (required)

Function to transform

param-renaming — (required)

A doublet or list of doublets

: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

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

:untranslate — default t

How to untranslate the function body after changing it.