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