		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-isuffix-option

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

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

Definitions and Theorems

Function: ldm-isuffix-option

(defun ldm-isuffix-option (isuffix?)
  (declare (xargs :guard (isuffix-optionp isuffix?)))
  (let ((__function__ 'ldm-isuffix-option))
    (declare (ignorable __function__))
    (isuffix-option-case isuffix?
                         :some (ldm-isuffix isuffix?.val)
                         :none (mv (c::iconst-length-none) nil))))

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

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

Theorem: booleanp-of-ldm-isuffix-option.unsignedp

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

Theorem: ldm-isuffix-option-of-isuffix-option-fix-isuffix?

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

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

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