		Search-engine friendly clone of the ACL2 documentation.

Type

Typep

Recognizer for type structures.

Signature
(typep x) → *

Definitions and Theorems

Function: typep

(defun typep (x)
  (declare (xargs :guard t))
  (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: consp-when-typep

(defthm consp-when-typep
  (implies (typep x) (consp x))
  :rule-classes :compound-recognizer)