• Top

• Sv::vl-moddb.lisp

Svex-lhs-from-name

Signature

(svex-lhs-from-name name &key (width '1) (rsh '0)) → lhs

Arguments

name — Guard (stringp name).

width — Guard (posp width).

rsh — Guard (natp rsh).

Returns

lhs — Type (sv::lhs-p lhs).

Definitions and Theorems

Function: svex-lhs-from-name-fn

(defun svex-lhs-from-name-fn (name width rsh)
 (declare (xargs :guard (and (stringp name)
                             (posp width)
                             (natp rsh))))
 (let ((__function__ 'svex-lhs-from-name))
  (declare (ignorable __function__))
  (list
    (sv::make-lhrange
         :w width
         :atom (sv::make-lhatom-var :name (svex-svar-from-name name)
                                    :rsh rsh)))))

Theorem: lhs-p-of-svex-lhs-from-name

(defthm lhs-p-of-svex-lhs-from-name
  (b* ((lhs (svex-lhs-from-name-fn name width rsh)))
    (sv::lhs-p lhs))
  :rule-classes :rewrite)

Theorem: svarlist-addr-p-of-svex-lhs-from-name

(defthm svarlist-addr-p-of-svex-lhs-from-name
  (b* ((?lhs (svex-lhs-from-name-fn name width rsh)))
    (sv::svarlist-addr-p (sv::lhs-vars lhs))))

Theorem: svex-lhs-from-name-fn-of-str-fix-name

(defthm svex-lhs-from-name-fn-of-str-fix-name
  (equal (svex-lhs-from-name-fn (str-fix name)
                                width rsh)
         (svex-lhs-from-name-fn name width rsh)))

Theorem: svex-lhs-from-name-fn-streqv-congruence-on-name

(defthm svex-lhs-from-name-fn-streqv-congruence-on-name
  (implies (streqv name name-equiv)
           (equal (svex-lhs-from-name-fn name width rsh)
                  (svex-lhs-from-name-fn name-equiv width rsh)))
  :rule-classes :congruence)

Theorem: svex-lhs-from-name-fn-of-pos-fix-width

(defthm svex-lhs-from-name-fn-of-pos-fix-width
  (equal (svex-lhs-from-name-fn name (pos-fix width)
                                rsh)
         (svex-lhs-from-name-fn name width rsh)))

Theorem: svex-lhs-from-name-fn-pos-equiv-congruence-on-width

(defthm svex-lhs-from-name-fn-pos-equiv-congruence-on-width
  (implies (acl2::pos-equiv width width-equiv)
           (equal (svex-lhs-from-name-fn name width rsh)
                  (svex-lhs-from-name-fn name width-equiv rsh)))
  :rule-classes :congruence)

Theorem: svex-lhs-from-name-fn-of-nfix-rsh

(defthm svex-lhs-from-name-fn-of-nfix-rsh
  (equal (svex-lhs-from-name-fn name width (nfix rsh))
         (svex-lhs-from-name-fn name width rsh)))

Theorem: svex-lhs-from-name-fn-nat-equiv-congruence-on-rsh

(defthm svex-lhs-from-name-fn-nat-equiv-congruence-on-rsh
  (implies (acl2::nat-equiv rsh rsh-equiv)
           (equal (svex-lhs-from-name-fn name width rsh)
                  (svex-lhs-from-name-fn name width rsh-equiv)))
  :rule-classes :congruence)