rawp-tests

(in-package "ACL2")

(assert! (rawp 'len state))

(assert! (rawp 'fmt-to-comment-window state))

(assert! (rawp 'floor state))

(assert! (rawp 'cw-gstack-fn state))

(assert! (rawp 'certify-book-fn state))

(assert! (rawp 'ev-w state))

(assert! (not (rawp 'cons state)))

(assert! (not (rawp 'parilis$ state)))

(must-succeed* (defun f (x) x)
  (assert! (not (rawp 'f state))))