		Search-engine friendly clone of the ACL2 documentation.

Types

Integer-type-xdoc-string

Documentation (sub)string that describes a C integer type.

Signature
(integer-type-xdoc-string type) → string
Arguments: type — Guard (typep type).
Returns: string — Type (stringp string).

Definitions and Theorems

Function: integer-type-xdoc-string

(defun integer-type-xdoc-string (type)
  (declare (xargs :guard (typep type)))
  (declare (xargs :guard (type-integerp type)))
  (let ((__function__ 'integer-type-xdoc-string))
    (declare (ignorable __function__))
    (b* ((core (case (type-kind type)
                 (:char "char")
                 (:schar "signed char")
                 (:uchar "unsigned char")
                 (:sshort "signed short")
                 (:ushort "unsigned short")
                 (:sint "signed int")
                 (:uint "unsigned int")
                 (:slong "signed long")
                 (:ulong "unsigned long")
                 (:sllong "signed long long")
                 (:ullong "unsigned long long")
                 (t (prog2$ (impossible) "")))))
      (str::cat "type @('" core "')"))))

Theorem: stringp-of-integer-type-xdoc-string

(defthm stringp-of-integer-type-xdoc-string
  (b* ((string (integer-type-xdoc-string type)))
    (stringp string))
  :rule-classes :rewrite)

Theorem: integer-type-xdoc-string-of-type-fix-type

(defthm integer-type-xdoc-string-of-type-fix-type
  (equal (integer-type-xdoc-string (type-fix type))
         (integer-type-xdoc-string type)))

Theorem: integer-type-xdoc-string-type-equiv-congruence-on-type

(defthm integer-type-xdoc-string-type-equiv-congruence-on-type
  (implies (type-equiv type type-equiv)
           (equal (integer-type-xdoc-string type)
                  (integer-type-xdoc-string type-equiv)))
  :rule-classes :congruence)