		Search-engine friendly clone of the ACL2 documentation.

Verilog-printing

Vl-pp-modulename-link-aux

Signature
(vl-pp-modulename-link-aux name origname &key (ps 'ps)) → ps
Arguments: name — Guard (stringp name).; origname — Guard (stringp origname).

Definitions and Theorems

Function: vl-pp-modulename-link-aux-fn

(defun vl-pp-modulename-link-aux-fn (name origname ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard (and (stringp name)
                              (stringp origname))))
  (declare (ignorable name))
  (let ((__function__ 'vl-pp-modulename-link-aux))
    (declare (ignorable __function__))
    (b* ((origname (string-fix origname)))
      (vl-print-modname origname))))

Theorem: vl-pp-modulename-link-aux-fn-of-str-fix-name

(defthm vl-pp-modulename-link-aux-fn-of-str-fix-name
  (equal (vl-pp-modulename-link-aux-fn (str-fix name)
                                       origname ps)
         (vl-pp-modulename-link-aux-fn name origname ps)))

Theorem: vl-pp-modulename-link-aux-fn-streqv-congruence-on-name

(defthm vl-pp-modulename-link-aux-fn-streqv-congruence-on-name
 (implies
      (streqv name name-equiv)
      (equal (vl-pp-modulename-link-aux-fn name origname ps)
             (vl-pp-modulename-link-aux-fn name-equiv origname ps)))
 :rule-classes :congruence)

Theorem: vl-pp-modulename-link-aux-fn-of-str-fix-origname

(defthm vl-pp-modulename-link-aux-fn-of-str-fix-origname
  (equal (vl-pp-modulename-link-aux-fn name (str-fix origname)
                                       ps)
         (vl-pp-modulename-link-aux-fn name origname ps)))

Theorem: vl-pp-modulename-link-aux-fn-streqv-congruence-on-origname

(defthm vl-pp-modulename-link-aux-fn-streqv-congruence-on-origname
 (implies
      (streqv origname origname-equiv)
      (equal (vl-pp-modulename-link-aux-fn name origname ps)
             (vl-pp-modulename-link-aux-fn name origname-equiv ps)))
 :rule-classes :congruence)