		Search-engine friendly clone of the ACL2 documentation.

Representation-of-integers

Integer-from-cinteger

ACL2 integer corresponding to the C integer.

Signature
(integer-from-cinteger cint) → int
Arguments: cint — Guard (cintegerp cint).
Returns: int — Type (integerp int).

Definitions and Theorems

Function: integer-from-cinteger

(defun integer-from-cinteger (cint)
  (declare (xargs :guard (cintegerp cint)))
  (let ((__function__ 'integer-from-cinteger))
    (declare (ignorable __function__))
    (cinteger-case cint
                   :schar (integer-from-schar cint.get)
                   :uchar (integer-from-uchar cint.get)
                   :sshort (integer-from-sshort cint.get)
                   :ushort (integer-from-ushort cint.get)
                   :sint (integer-from-sint cint.get)
                   :uint (integer-from-uint cint.get)
                   :slong (integer-from-slong cint.get)
                   :ulong (integer-from-ulong cint.get)
                   :sllong (integer-from-sllong cint.get)
                   :ullong (integer-from-ullong cint.get))))

Theorem: integerp-of-integer-from-cinteger

(defthm integerp-of-integer-from-cinteger
  (b* ((int (integer-from-cinteger cint)))
    (integerp int))
  :rule-classes :rewrite)

Theorem: integer-from-cinteger-alt-def

(defthm integer-from-cinteger-alt-def
  (equal (integer-from-cinteger x)
         (cond ((scharp x) (integer-from-schar x))
               ((ucharp x) (integer-from-uchar x))
               ((sshortp x) (integer-from-sshort x))
               ((ushortp x) (integer-from-ushort x))
               ((sintp x) (integer-from-sint x))
               ((uintp x) (integer-from-uint x))
               ((slongp x) (integer-from-slong x))
               ((ulongp x) (integer-from-ulong x))
               ((sllongp x) (integer-from-sllong x))
               (t (integer-from-ullong x)))))

Theorem: integer-from-cinteger-of-cinteger-fix-cint

(defthm integer-from-cinteger-of-cinteger-fix-cint
  (equal (integer-from-cinteger (cinteger-fix cint))
         (integer-from-cinteger cint)))

Theorem: integer-from-cinteger-cinteger-equiv-congruence-on-cint

(defthm integer-from-cinteger-cinteger-equiv-congruence-on-cint
  (implies (cinteger-equiv cint cint-equiv)
           (equal (integer-from-cinteger cint)
                  (integer-from-cinteger cint-equiv)))
  :rule-classes :congruence)