		Search-engine friendly clone of the ACL2 documentation.

Selfassigns

Vl-selfassign-bit

Signature
(vl-selfassign-bit name index) → bit
Arguments: name — Guard (stringp name).; index — Guard (integerp index).
Returns: bit — Type (stringp bit).

Definitions and Theorems

Function: vl-selfassign-bit

(defun vl-selfassign-bit (name index)
  (declare (xargs :guard (and (stringp name) (integerp index))))
  (let ((__function__ 'vl-selfassign-bit))
    (declare (ignorable __function__))
    (b* ((index (lifix index)))
      (cat name "[" (if (< index 0) "-" "")
           (natstr (abs index))
           "]"))))

Theorem: stringp-of-vl-selfassign-bit

(defthm stringp-of-vl-selfassign-bit
  (b* ((bit (vl-selfassign-bit name index)))
    (stringp bit))
  :rule-classes :type-prescription)

Theorem: vl-selfassign-bit-of-str-fix-name

(defthm vl-selfassign-bit-of-str-fix-name
  (equal (vl-selfassign-bit (str-fix name) index)
         (vl-selfassign-bit name index)))

Theorem: vl-selfassign-bit-streqv-congruence-on-name

(defthm vl-selfassign-bit-streqv-congruence-on-name
  (implies (streqv name name-equiv)
           (equal (vl-selfassign-bit name index)
                  (vl-selfassign-bit name-equiv index)))
  :rule-classes :congruence)

Theorem: vl-selfassign-bit-of-ifix-index

(defthm vl-selfassign-bit-of-ifix-index
  (equal (vl-selfassign-bit name (ifix index))
         (vl-selfassign-bit name index)))

Theorem: vl-selfassign-bit-int-equiv-congruence-on-index

(defthm vl-selfassign-bit-int-equiv-congruence-on-index
  (implies (acl2::int-equiv index index-equiv)
           (equal (vl-selfassign-bit name index)
                  (vl-selfassign-bit name index-equiv)))
  :rule-classes :congruence)