		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-isuffix

Map an integer suffix to an integer constant length in the language definition and to an unsigned flag.

Signature
(ldm-isuffix isuffix) → (mv ilen unsignedp)
Arguments: isuffix — Guard (isuffixp isuffix).
Returns: ilen — Type (c::iconst-lengthp ilen).; unsignedp — Type (booleanp unsignedp).

Definitions and Theorems

Function: ldm-isuffix

(defun ldm-isuffix (isuffix)
  (declare (xargs :guard (isuffixp isuffix)))
  (let ((__function__ 'ldm-isuffix))
    (declare (ignorable __function__))
    (isuffix-case isuffix
                  :u (mv (c::iconst-length-none) t)
                  :l (mv (ldm-lsuffix isuffix.length) nil)
                  :ul (mv (ldm-lsuffix isuffix.length) t)
                  :lu (mv (ldm-lsuffix isuffix.length) t))))

Theorem: iconst-lengthp-of-ldm-isuffix.ilen

(defthm iconst-lengthp-of-ldm-isuffix.ilen
  (b* (((mv ?ilen ?unsignedp)
        (ldm-isuffix isuffix)))
    (c::iconst-lengthp ilen))
  :rule-classes :rewrite)

Theorem: booleanp-of-ldm-isuffix.unsignedp

(defthm booleanp-of-ldm-isuffix.unsignedp
  (b* (((mv ?ilen ?unsignedp)
        (ldm-isuffix isuffix)))
    (booleanp unsignedp))
  :rule-classes :rewrite)

Theorem: ldm-isuffix-of-isuffix-fix-isuffix

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

Theorem: ldm-isuffix-isuffix-equiv-congruence-on-isuffix

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