		Search-engine friendly clone of the ACL2 documentation.

Stv-expand

Stv-expand-hid

(stv-expand-hid name mod) expands a signal name when it is allowed to be hierarchical, i.e. a hid or a list of esim paths.

Signature
(stv-expand-hid name mod) → lsb-paths
Arguments: name — the name at the start of the STV line.
Returns: lsb-paths — LSB-first list of non-canonical paths for x, in the sense of mod-internal-paths.

Definitions and Theorems

Function: stv-expand-hid

(defun stv-expand-hid (name mod)
  (declare (xargs :guard t))
  (let ((__function__ 'stv-expand-hid))
    (declare (ignorable __function__))
    (if (stringp name)
        (stv-hid-to-paths name mod)
      (prog2$ (stv-check-noncanonical-paths name mod)
              name))))