		Search-engine friendly clone of the ACL2 documentation.

Type

Type-kind

Get the kind (tag) of a type structure.

Signature
(type-kind x) → kind
Arguments: x — Guard (typep x).

Definitions and Theorems

Function: type-kind$inline

(defun type-kind$inline (x)
  (declare (xargs :guard (typep x)))
  (mbe :logic (cond ((or (atom x) (eq (car x) :void)) :void)
                    ((eq (car x) :char) :char)
                    ((eq (car x) :schar) :schar)
                    ((eq (car x) :uchar) :uchar)
                    ((eq (car x) :sshort) :sshort)
                    ((eq (car x) :ushort) :ushort)
                    ((eq (car x) :sint) :sint)
                    ((eq (car x) :uint) :uint)
                    ((eq (car x) :slong) :slong)
                    ((eq (car x) :ulong) :ulong)
                    ((eq (car x) :sllong) :sllong)
                    ((eq (car x) :ullong) :ullong)
                    ((eq (car x) :struct) :struct)
                    ((eq (car x) :pointer) :pointer)
                    (t :array))
       :exec (car x)))

Theorem: type-kind-possibilities

(defthm type-kind-possibilities
 (or (equal (type-kind x) :void)
     (equal (type-kind x) :char)
     (equal (type-kind x) :schar)
     (equal (type-kind x) :uchar)
     (equal (type-kind x) :sshort)
     (equal (type-kind x) :ushort)
     (equal (type-kind x) :sint)
     (equal (type-kind x) :uint)
     (equal (type-kind x) :slong)
     (equal (type-kind x) :ulong)
     (equal (type-kind x) :sllong)
     (equal (type-kind x) :ullong)
     (equal (type-kind x) :struct)
     (equal (type-kind x) :pointer)
     (equal (type-kind x) :array))
 :rule-classes ((:forward-chaining :trigger-terms ((type-kind x)))))