		Search-engine friendly clone of the ACL2 documentation.

Stv-compile

Stv-forge-state-bit

Generate the name for a state bit, like foo!bar!baz!inst!S, given a list of instance names and the name of the state bit.

Signature
(stv-forge-state-bit instnames st-name) → full-name
Arguments: instnames — List of instance names.; st-name — Guard (atom st-name).
Returns: full-name — Type (atom full-name), given the guard.

Definitions and Theorems

Function: stv-forge-state-bit

(defun stv-forge-state-bit (instnames st-name)
       (declare (xargs :guard (atom st-name)))
       (let ((__function__ 'stv-forge-state-bit))
            (declare (ignorable __function__))
            (if (atom instnames)
                st-name
                (prefix-atom (stringify (car instnames))
                             "!"
                             (stv-forge-state-bit (cdr instnames)
                                                  st-name)))))

Theorem: atom-of-stv-forge-state-bit

(defthm
  atom-of-stv-forge-state-bit
  (implies (and (atom st-name))
           (b* ((full-name (stv-forge-state-bit instnames st-name)))
               (atom full-name)))
  :rule-classes :rewrite)