Function:
(defun vl-lucid-mash-tag (x) (declare (xargs :guard (stringp x))) (let ((__function__ 'vl-lucid-mash-tag)) (declare (ignorable __function__)) (b* ((x (string-fix x)) (x (str::strsubst "VL-" "" x)) (x (str::strsubst "DECL" "" x)) (x (str::downcase-string x))) x)))
Theorem:
(defthm stringp-of-vl-lucid-mash-tag (b* ((new-x (vl-lucid-mash-tag x))) (stringp new-x)) :rule-classes :type-prescription)
Theorem:
(defthm vl-lucid-mash-tag-of-str-fix-x (equal (vl-lucid-mash-tag (str-fix x)) (vl-lucid-mash-tag x)))
Theorem:
(defthm vl-lucid-mash-tag-streqv-congruence-on-x (implies (streqv x x-equiv) (equal (vl-lucid-mash-tag x) (vl-lucid-mash-tag x-equiv))) :rule-classes :congruence)