		Search-engine friendly clone of the ACL2 documentation.

Vl-unparam-basename

Vl-unparam-basename-paramdecls

Signature
(vl-unparam-basename-paramdecls x include-default &key (ps 'ps)) → ps
Arguments: x — Guard (vl-paramdecllist-p x).; include-default — Guard (booleanp include-default).

Definitions and Theorems

Function: vl-unparam-basename-paramdecls-fn

(defun vl-unparam-basename-paramdecls-fn (x include-default ps)
 (declare (xargs :stobjs (ps)))
 (declare (xargs :guard (and (vl-paramdecllist-p x)
                             (booleanp include-default))))
 (let ((__function__ 'vl-unparam-basename-paramdecls))
  (declare (ignorable __function__))
  (b*
   (((when (atom x)) ps)
    ((vl-paramdecl x1) (car x))
    ((when (or x1.localp
               (and (not include-default)
                    (not x1.overriddenp))))
     (vl-unparam-basename-paramdecls (cdr x)
                                     include-default))
    ((the string name-part)
     (common-lisp::substitute #\_ #\Space x1.name))
    ((the string type-expr-part)
     (vl-paramtype-case
          x1.type :vl-implicitvalueparam
          (vl-unparam-basename-exprstring x1.type.default)
          :vl-explicitvalueparam
          (vl-unparam-basename-exprstring x1.type.default)
          :vl-typeparam
          (if x1.type.default
              (common-lisp::substitute
                   #\_ #\Space
                   (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-basename-paramdecls (cdr x)
                                              include-default)))))

Theorem: vl-unparam-basename-paramdecls-fn-of-vl-paramdecllist-fix-x

(defthm vl-unparam-basename-paramdecls-fn-of-vl-paramdecllist-fix-x
  (equal (vl-unparam-basename-paramdecls-fn (vl-paramdecllist-fix x)
                                            include-default ps)
         (vl-unparam-basename-paramdecls-fn x include-default ps)))

Theorem: vl-unparam-basename-paramdecls-fn-vl-paramdecllist-equiv-congruence-on-x

(defthm
 vl-unparam-basename-paramdecls-fn-vl-paramdecllist-equiv-congruence-on-x
 (implies
  (vl-paramdecllist-equiv x x-equiv)
  (equal
    (vl-unparam-basename-paramdecls-fn x include-default ps)
    (vl-unparam-basename-paramdecls-fn x-equiv include-default ps)))
 :rule-classes :congruence)

Theorem: vl-unparam-basename-paramdecls-fn-of-bool-fix-include-default

(defthm
      vl-unparam-basename-paramdecls-fn-of-bool-fix-include-default
  (equal (vl-unparam-basename-paramdecls-fn
              x (acl2::bool-fix include-default)
              ps)
         (vl-unparam-basename-paramdecls-fn x include-default ps)))

Theorem: vl-unparam-basename-paramdecls-fn-iff-congruence-on-include-default

(defthm
 vl-unparam-basename-paramdecls-fn-iff-congruence-on-include-default
 (implies
  (iff include-default include-default-equiv)
  (equal
    (vl-unparam-basename-paramdecls-fn x include-default ps)
    (vl-unparam-basename-paramdecls-fn x include-default-equiv ps)))
 :rule-classes :congruence)