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