(vl-tack-scopes-onto-hid scopes hid) → expr
Function:
(defun vl-tack-scopes-onto-hid (scopes hid) (declare (xargs :guard (and (vl-exprlist-p scopes) (vl-expr-p hid)))) (let ((__function__ 'vl-tack-scopes-onto-hid)) (declare (ignorable __function__)) (if (atom scopes) (vl-expr-fix hid) (make-vl-nonatom :op :vl-scope :args (list (car scopes) (vl-tack-scopes-onto-hid (cdr scopes) hid))))))
Theorem:
(defthm vl-expr-p-of-vl-tack-scopes-onto-hid (b* ((expr (vl-tack-scopes-onto-hid scopes hid))) (vl-expr-p expr)) :rule-classes :rewrite)