Function:
(defun vl-lint-throwaway-fn-p (x) (declare (xargs :guard (vl-stmt-p x))) (let ((__function__ 'vl-lint-throwaway-fn-p)) (declare (ignorable __function__)) (b* (((unless (vl-enablestmt-p x)) nil) ((vl-enablestmt x) x) ((unless (vl-fast-atom-p x.id)) nil) ((vl-atom x.id) x.id) ((unless (vl-fast-sysfunname-p x.id.guts)) nil) ((vl-sysfunname x.id.guts) x.id.guts)) (and (member-equal x.id.guts.name (list "$display" "$vcover" "$verror" "$acc_readmem")) t))))
Theorem:
(defthm booleanp-of-vl-lint-throwaway-fn-p (b* ((throwaway-p (vl-lint-throwaway-fn-p x))) (booleanp throwaway-p)) :rule-classes :type-prescription)
Theorem:
(defthm vl-lint-throwaway-fn-p-of-vl-stmt-fix-x (equal (vl-lint-throwaway-fn-p (vl-stmt-fix x)) (vl-lint-throwaway-fn-p x)))
Theorem:
(defthm vl-lint-throwaway-fn-p-vl-stmt-equiv-congruence-on-x (implies (vl-stmt-equiv x x-equiv) (equal (vl-lint-throwaway-fn-p x) (vl-lint-throwaway-fn-p x-equiv))) :rule-classes :congruence)