		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-enumer

Map an enumerator to an identifier in the language definition.

Signature
(ldm-enumer enumer) → (mv erp ident)
Arguments: enumer — Guard (enumerp enumer).
Returns: ident — Type (c::identp ident).

We only support enumerators without expression, so they are really just identifiers.

Definitions and Theorems

Function: ldm-enumer

(defun ldm-enumer (enumer)
  (declare (xargs :guard (enumerp enumer)))
  (declare (xargs :guard (enumer-unambp enumer)))
  (let ((__function__ 'ldm-enumer))
    (declare (ignorable __function__))
    (b* (((reterr) (c::ident "irrelevant"))
         ((enumer enumer) enumer)
         ((when enumer.value)
          (reterr (msg "Unsupported enumerator ~x0."
                       (enumer-fix enumer)))))
      (ldm-ident enumer.name))))

Theorem: identp-of-ldm-enumer.ident

(defthm identp-of-ldm-enumer.ident
  (b* (((mv acl2::?erp ?ident)
        (ldm-enumer enumer)))
    (c::identp ident))
  :rule-classes :rewrite)

Theorem: ldm-enumer-of-enumer-fix-enumer

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

Theorem: ldm-enumer-enumer-equiv-congruence-on-enumer

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