Types allowed in Smtlink.
(smt-typep term) → valid-type?
Function:
(defun smt-typep (term) (declare (xargs :guard t)) (let ((acl2::__function__ 'smt-typep)) (declare (ignorable acl2::__function__)) (symbolp term)))
Theorem:
(defthm booleanp-of-smt-typep (b* ((valid-type? (smt-typep term))) (booleanp valid-type?)) :rule-classes :rewrite)