		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-initer

Map an initializer to an initializer in the language definition.

Signature
(ldm-initer initer) → (mv erp initer1)
Arguments: initer — Guard (initerp initer).
Returns: initer1 — Type (c::initerp initer1).

Definitions and Theorems

Function: ldm-initer

(defun ldm-initer (initer)
  (declare (xargs :guard (initerp initer)))
  (declare (xargs :guard (initer-unambp initer)))
  (let ((__function__ 'ldm-initer))
    (declare (ignorable __function__))
    (b* (((reterr) (c::initer-list nil)))
      (initer-case initer :single
                   (b* (((erp expr1) (ldm-expr initer.expr)))
                     (retok (c::initer-single expr1)))
                   :list
                   (b* (((erp exprs1)
                         (ldm-desiniter-list initer.elems)))
                     (retok (c::initer-list exprs1)))))))

Theorem: initerp-of-ldm-initer.initer1

(defthm initerp-of-ldm-initer.initer1
  (b* (((mv acl2::?erp ?initer1)
        (ldm-initer initer)))
    (c::initerp initer1))
  :rule-classes :rewrite)

Theorem: ldm-initer-ok-when-initer-formalp

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

Theorem: ldm-initer-of-initer-fix-initer

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

Theorem: ldm-initer-initer-equiv-congruence-on-initer

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