(svex-svar-from-name name) → svar
Function:
(defun svex-svar-from-name (name) (declare (xargs :guard (stringp name))) (let ((__function__ 'svex-svar-from-name)) (declare (ignorable __function__)) (sv::make-svar :name (sv::make-address :path (sv::make-path-wire :name (string-fix name))))))
Theorem:
(defthm svar-p-of-svex-svar-from-name (b* ((svar (svex-svar-from-name name))) (sv::svar-p svar)) :rule-classes :rewrite)
Theorem:
(defthm svar-addr-p-of-svex-svar-from-name (b* ((?svar (svex-svar-from-name name))) (sv::svar-addr-p svar)))
Theorem:
(defthm svex-svar-from-name-of-str-fix-name (equal (svex-svar-from-name (str-fix name)) (svex-svar-from-name name)))
Theorem:
(defthm svex-svar-from-name-streqv-congruence-on-name (implies (streqv name name-equiv) (equal (svex-svar-from-name name) (svex-svar-from-name name-equiv))) :rule-classes :congruence)