		Search-engine friendly clone of the ACL2 documentation.

Drop-irrelevant-params

Removes some irrelevant parameters from a function.

General Form:

(drop-irrelevant-params fn
                        param-or-params-to-drop
                        &key
                        :show-only              ; default nil
                        :print                  ; default :result
                        :new-name               ; default :auto
                        :build-wrapper          ; default nil
                        :theorem-disabled       ; default nil
                        :function-disabled      ; default :auto
                        :measure-hints          ; default :auto
                        :verify-guards          ; default :auto
                        :guard-hints            ; default :auto
                        :untranslate            ; default :macros
                        )

Inputs:

fn — (required)

The function to transform (a defined function).

param-or-params-to-drop — (required)

The param to drop (a symbol), or a list of such.

: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 new name to use, or :auto to have the transformation generate a name. If the target function is defined in a mutual-recursion, we support :map syntax for the :new-name option.

:build-wrapper — default nil

Whether to build a wrapper function.

:theorem-disabled — default nil

Whether to disable the 'becomes theorem'.

:function-disabled — default :auto

Whether to disable the new function.

:measure-hints — default :auto

Hints to use for the measure/termination proof.

:verify-guards — default :auto

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

:guard-hints — default :auto

Hints to use for the guard proof.

:untranslate — default :macros

How to untranslate the function body after changing it.

Description:

An irrelevant parameter is one that is not used in the body of the function except (perhaps) to calculate new values for the same parameter in recursive calls.

This transform supports dropping multiple irrelevant parameters simultaneously. (I suppose all irrelevant parameters can be used to generate new values for any other irrelevant parameters -- and still be considered irrelevant).