Recognizer for type structures.
(typep x) → *
Function:
(defun typep (x) (declare (xargs :guard t)) (let ((__function__ 'typep)) (declare (ignorable __function__)) (and (consp x) (cond ((or (atom x) (eq (car x) :void)) (and (true-listp (cdr x)) (eql (len (cdr x)) 0) (b* nil t))) ((eq (car x) :char) (and (true-listp (cdr x)) (eql (len (cdr x)) 0) (b* nil t))) ((eq (car x) :schar) (and (true-listp (cdr x)) (eql (len (cdr x)) 0) (b* nil t))) ((eq (car x) :uchar) (and (true-listp (cdr x)) (eql (len (cdr x)) 0) (b* nil t))) ((eq (car x) :sshort) (and (true-listp (cdr x)) (eql (len (cdr x)) 0) (b* nil t))) ((eq (car x) :ushort) (and (true-listp (cdr x)) (eql (len (cdr x)) 0) (b* nil t))) ((eq (car x) :sint) (and (true-listp (cdr x)) (eql (len (cdr x)) 0) (b* nil t))) ((eq (car x) :uint) (and (true-listp (cdr x)) (eql (len (cdr x)) 0) (b* nil t))) ((eq (car x) :slong) (and (true-listp (cdr x)) (eql (len (cdr x)) 0) (b* nil t))) ((eq (car x) :ulong) (and (true-listp (cdr x)) (eql (len (cdr x)) 0) (b* nil t))) ((eq (car x) :sllong) (and (true-listp (cdr x)) (eql (len (cdr x)) 0) (b* nil t))) ((eq (car x) :ullong) (and (true-listp (cdr x)) (eql (len (cdr x)) 0) (b* nil t))) ((eq (car x) :struct) (and (true-listp (cdr x)) (eql (len (cdr x)) 1) (b* ((tag (std::da-nth 0 (cdr x)))) (identp tag)))) ((eq (car x) :pointer) (and (true-listp (cdr x)) (eql (len (cdr x)) 1) (b* ((to (std::da-nth 0 (cdr x)))) (typep to)))) (t (and (eq (car x) :array) (and (true-listp (cdr x)) (eql (len (cdr x)) 2)) (b* ((of (std::da-nth 0 (cdr x))) (size (std::da-nth 1 (cdr x)))) (and (typep of) (pos-optionp size)))))))))
Theorem:
(defthm consp-when-typep (implies (typep x) (consp x)) :rule-classes :compound-recognizer)