		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-const

Map a constant to a constant in the language definition.

Signature
(ldm-const const) → (mv erp const1)
Arguments: const — Guard (constp const).
Returns: const1 — Type (c::constp const1).

Definitions and Theorems

Function: ldm-const

(defun ldm-const (const)
  (declare (xargs :guard (constp const)))
  (let ((__function__ 'ldm-const))
    (declare (ignorable __function__))
    (b* (((reterr)
          (c::const-enum (c::ident "irrelevant"))))
      (const-case
           const :int
           (retok (c::const-int (ldm-iconst const.unwrap)))
           :float
           (reterr (msg "Unsupported floating constant ~x0."
                        const.unwrap))
           :enum
           (b* (((erp ident1) (ldm-ident const.unwrap)))
             (retok (c::const-enum ident1)))
           :char (reterr (msg "Unsupported character constant ~x0."
                              const.unwrap))))))

Theorem: constp-of-ldm-const.const1

(defthm constp-of-ldm-const.const1
  (b* (((mv acl2::?erp ?const1)
        (ldm-const const)))
    (c::constp const1))
  :rule-classes :rewrite)

Theorem: ldm-const-ok-when-const-formalp

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

Theorem: ldm-const-of-const-fix-const

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

Theorem: ldm-const-const-equiv-congruence-on-const

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