		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-ident

Map an identiifer to an identifier in the language definition.

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

Since the language definition requires ACL2 strings, we throw an error if the identifier is not an ACL2 string.

Definitions and Theorems

Function: ldm-ident

(defun ldm-ident (ident)
  (declare (xargs :guard (identp ident)))
  (let ((__function__ 'ldm-ident))
    (declare (ignorable __function__))
    (b* (((reterr) (c::ident "irrelevant"))
         (string (ident->unwrap ident))
         ((unless (stringp string))
          (reterr (msg "Unsupported identifier with non-string ~x0."
                       string))))
      (retok (c::ident string)))))

Theorem: identp-of-ldm-ident.ident1

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

Theorem: ldm-ident-ok-when-ident-formalp

(defthm ldm-ident-ok-when-ident-formalp
  (implies (ident-formalp ident)
           (b* (((mv acl2::?erp ?ident1)
                 (ldm-ident ident)))
             (not erp))))

Theorem: ldm-ident-of-ident-fix-ident

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

Theorem: ldm-ident-ident-equiv-congruence-on-ident

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