		Search-engine friendly clone of the ACL2 documentation.

Types

nonchar-integer-types

List of the (supported) C integer types except plain char.

Definition: *nonchar-integer-types*

(defconst *nonchar-integer-types*
  (list (type-schar)
        (type-uchar)
        (type-sshort)
        (type-ushort)
        (type-sint)
        (type-uint)
        (type-slong)
        (type-ulong)
        (type-sllong)
        (type-ullong)))

Definitions and Theorems

Theorem: member-nonchar-integer-types-as-pred

(defthm member-nonchar-integer-types-as-pred
  (implies (typep type)
           (iff (member-equal type *nonchar-integer-types*)
                (type-nonchar-integerp type))))