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) :float) (and (true-listp (cdr x)) (eql (len (cdr x)) 0) (b* nil t))) ((eq (car x) :double) (and (true-listp (cdr x)) (eql (len (cdr x)) 0) (b* nil t))) ((eq (car x) :ldouble) (and (true-listp (cdr x)) (eql (len (cdr x)) 0) (b* nil t))) ((eq (car x) :floatc) (and (true-listp (cdr x)) (eql (len (cdr x)) 0) (b* nil t))) ((eq (car x) :doublec) (and (true-listp (cdr x)) (eql (len (cdr x)) 0) (b* nil t))) ((eq (car x) :ldoublec) (and (true-listp (cdr x)) (eql (len (cdr x)) 0) (b* nil t))) ((eq (car x) :bool) (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)) 0) (b* nil t))) ((eq (car x) :union) (and (true-listp (cdr x)) (eql (len (cdr x)) 0) (b* nil t))) ((eq (car x) :enum) (and (true-listp (cdr x)) (eql (len (cdr x)) 0) (b* nil t))) ((eq (car x) :array) (and (true-listp (cdr x)) (eql (len (cdr x)) 0) (b* nil t))) ((eq (car x) :pointer) (and (true-listp (cdr x)) (eql (len (cdr x)) 0) (b* nil t))) ((eq (car x) :function) (and (true-listp (cdr x)) (eql (len (cdr x)) 0) (b* nil t))) (t (and (eq (car x) :unknown) (and (true-listp (cdr x)) (eql (len (cdr x)) 0)) (b* nil t)))))))
Theorem:
(defthm consp-when-typep (implies (typep x) (consp x)) :rule-classes :compound-recognizer)