		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-iconst

Map an integer constant to an integer constant in the language definition.

Signature
(ldm-iconst iconst) → iconst1
Arguments: iconst — Guard (iconstp iconst).
Returns: iconst1 — Type (c::iconstp iconst1).

Definitions and Theorems

Function: ldm-iconst

(defun ldm-iconst (iconst)
  (declare (xargs :guard (iconstp iconst)))
  (let ((__function__ 'ldm-iconst))
    (declare (ignorable __function__))
    (b* (((iconst iconst) iconst)
         ((mv value base)
          (ldm-dec/oct/hex-const iconst.core))
         ((mv length unsignedp)
          (ldm-isuffix-option iconst.suffix?)))
      (c::make-iconst :value value
                      :base base
                      :unsignedp unsignedp
                      :length length))))

Theorem: iconstp-of-ldm-iconst

(defthm iconstp-of-ldm-iconst
  (b* ((iconst1 (ldm-iconst iconst)))
    (c::iconstp iconst1))
  :rule-classes :rewrite)

Theorem: ldm-iconst-of-iconst-fix-iconst

(defthm ldm-iconst-of-iconst-fix-iconst
  (equal (ldm-iconst (iconst-fix iconst))
         (ldm-iconst iconst)))

Theorem: ldm-iconst-iconst-equiv-congruence-on-iconst

(defthm ldm-iconst-iconst-equiv-congruence-on-iconst
  (implies (iconst-equiv iconst iconst-equiv)
           (equal (ldm-iconst iconst)
                  (ldm-iconst iconst-equiv)))
  :rule-classes :congruence)