		Search-engine friendly clone of the ACL2 documentation.

Vl-unparam-newname

Vl-unparam-newname-aux

Signature
(vl-unparam-newname-aux x &key (ps 'ps)) → ps
Arguments: x — Guard (vl-paramdecllist-p x).

Definitions and Theorems

Function: vl-unparam-newname-aux-fn

(defun vl-unparam-newname-aux-fn (x ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard (vl-paramdecllist-p x)))
  (let ((__function__ 'vl-unparam-newname-aux))
    (declare (ignorable __function__))
    (b* (((when (atom x)) ps)
         ((vl-paramdecl x1) (car x))
         ((when x1.localp)
          (vl-unparam-newname-aux (cdr x)))
         ((the string name-part)
          (common-lisp::substitute #\_ #\Space x1.name))
         ((the string type-expr-part)
          (vl-paramtype-case
               x1.type :vl-implicitvalueparam
               (vl-unparam-newname-exprstring x1.type.default)
               :vl-explicitvalueparam
               (vl-unparam-newname-exprstring x1.type.default)
               :vl-typeparam
               (if x1.type.default
                   (with-local-ps (vl-pp-datatype x1.type.default))
                 "NULL"))))
      (vl-ps-seq (vl-print "$")
                 (vl-print-str name-part)
                 (vl-print "=")
                 (vl-print-str type-expr-part)
                 (vl-unparam-newname-aux (cdr x))))))

Theorem: vl-unparam-newname-aux-fn-of-vl-paramdecllist-fix-x

(defthm vl-unparam-newname-aux-fn-of-vl-paramdecllist-fix-x
  (equal (vl-unparam-newname-aux-fn (vl-paramdecllist-fix x)
                                    ps)
         (vl-unparam-newname-aux-fn x ps)))

Theorem: vl-unparam-newname-aux-fn-vl-paramdecllist-equiv-congruence-on-x

(defthm
   vl-unparam-newname-aux-fn-vl-paramdecllist-equiv-congruence-on-x
  (implies (vl-paramdecllist-equiv x x-equiv)
           (equal (vl-unparam-newname-aux-fn x ps)
                  (vl-unparam-newname-aux-fn x-equiv ps)))
  :rule-classes :congruence)