(vl-foreachstmt->blockscope x) → scope
Function:
(defun vl-foreachstmt->blockscope (x) (declare (xargs :guard (vl-stmt-p x))) (declare (xargs :guard (vl-stmt-case x :vl-foreachstmt))) (let ((__function__ 'vl-foreachstmt->blockscope)) (declare (ignorable __function__)) (b* (((vl-foreachstmt x))) (make-vl-blockscope :vardecls x.vardecls :scopetype :vl-foreachstmt))))
Theorem:
(defthm vl-blockscope-p-of-vl-foreachstmt->blockscope (b* ((scope (vl-foreachstmt->blockscope x))) (vl-blockscope-p scope)) :rule-classes :rewrite)
Theorem:
(defthm vl-foreachstmt->blockscope-of-vl-stmt-fix-x (equal (vl-foreachstmt->blockscope (vl-stmt-fix x)) (vl-foreachstmt->blockscope x)))
Theorem:
(defthm vl-foreachstmt->blockscope-vl-stmt-equiv-congruence-on-x (implies (vl-stmt-equiv x x-equiv) (equal (vl-foreachstmt->blockscope x) (vl-foreachstmt->blockscope x-equiv))) :rule-classes :congruence)