		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 (natp 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) (natp index))))
  (let ((__function__ 'vl-selfassign-bit))
    (declare (ignorable __function__))
    (cat name "[" (natstr 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)