The function type-hyp passes type related information onto the trusted clause processor.
Function:
(defun type-hyp (blist tag) (declare (xargs :guard (and (boolean-listp blist) (symbolp tag)))) (let ((acl2::__function__ 'type-hyp)) (declare (ignorable acl2::__function__)) (b* ((blist (acl2::boolean-list-fix blist)) ((unless (consp blist)) t) ((cons first rest) blist)) (and first (type-hyp rest tag)))))