(vl-atomicstmt-cblock-pathcheck1 varname x) → bool
Function:
(defun vl-atomicstmt-cblock-pathcheck1 (varname x) (declare (xargs :guard (and (stringp varname) (and (vl-stmt-p x) (vl-atomicstmt-p x))))) (declare (xargs :guard (vl-atomicstmt-cblock-p x))) (let ((__function__ 'vl-atomicstmt-cblock-pathcheck1)) (declare (ignorable __function__)) (case (vl-stmt-kind x) (:vl-nullstmt nil) (:vl-assignstmt (equal (vl-idexpr->name (vl-assignstmt->lvalue x)) varname)) (otherwise nil))))
Theorem:
(defthm booleanp-of-vl-atomicstmt-cblock-pathcheck1 (b* ((bool (vl-atomicstmt-cblock-pathcheck1 varname x))) (booleanp bool)) :rule-classes :type-prescription)