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