		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-lsuffix

Map a length suffix to an integer constant length in the language definition.

Signature
(ldm-lsuffix lsuffix) → ilen
Arguments: lsuffix — Guard (lsuffixp lsuffix).
Returns: ilen — Type (c::iconst-lengthp ilen).

Definitions and Theorems

Function: ldm-lsuffix

(defun ldm-lsuffix (lsuffix)
  (declare (xargs :guard (lsuffixp lsuffix)))
  (let ((__function__ 'ldm-lsuffix))
    (declare (ignorable __function__))
    (lsuffix-case lsuffix
                  :locase-l (c::iconst-length-long)
                  :upcase-l (c::iconst-length-long)
                  :locase-ll (c::iconst-length-llong)
                  :upcase-ll (c::iconst-length-llong))))

Theorem: iconst-lengthp-of-ldm-lsuffix

(defthm iconst-lengthp-of-ldm-lsuffix
  (b* ((ilen (ldm-lsuffix lsuffix)))
    (c::iconst-lengthp ilen))
  :rule-classes :rewrite)

Theorem: ldm-lsuffix-of-lsuffix-fix-lsuffix

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

Theorem: ldm-lsuffix-lsuffix-equiv-congruence-on-lsuffix

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