		Search-engine friendly clone of the ACL2 documentation.

Clean-params

Vl-paramargs-elim-useless-params

Apply a vl-useless-params-p to clean up an vl-paramargs-p structure.

Signature
(vl-paramargs-elim-useless-params useless arguments) → new-arguments
Arguments: useless — Guard (vl-useless-params-p useless).; arguments — Guard (vl-paramargs-p arguments).
Returns: new-arguments — Type (vl-paramargs-p new-arguments), given (force (vl-paramargs-p arguments)).

Definitions and Theorems

Function: vl-paramargs-elim-useless-params

(defun vl-paramargs-elim-useless-params (useless arguments)
  (declare (xargs :guard (and (vl-useless-params-p useless)
                              (vl-paramargs-p arguments))))
  (let ((__function__ 'vl-paramargs-elim-useless-params))
    (declare (ignorable __function__))
    (b* (((vl-useless-params useless) useless))
      (vl-paramargs-case
           arguments
           :vl-paramargs-named
           (change-vl-paramargs-named
                arguments
                :args (vl-namedparamvaluelist-elim-useless-params
                           useless.names arguments.args))
           :vl-paramargs-plain
           (change-vl-paramargs-plain
                arguments.args
                :args (vl-paramvaluelist-elim-useless-params
                           0 useless.positions arguments.args))))))

Theorem: vl-paramargs-p-of-vl-paramargs-elim-useless-params

(defthm vl-paramargs-p-of-vl-paramargs-elim-useless-params
 (implies
    (force (vl-paramargs-p arguments))
    (b* ((new-arguments
              (vl-paramargs-elim-useless-params useless arguments)))
      (vl-paramargs-p new-arguments)))
 :rule-classes :rewrite)