		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-desiniter

Map an initializer with optional designations to an initializer expression in the language definition.

Signature
(ldm-desiniter desiniter) → (mv erp expr)
Arguments: desiniter — Guard (desiniterp desiniter).
Returns: expr — Type (c::exprp expr).

There must be no designators, and the nested initializer must be for a single expression.

Definitions and Theorems

Function: ldm-desiniter

(defun ldm-desiniter (desiniter)
  (declare (xargs :guard (desiniterp desiniter)))
  (declare (xargs :guard (desiniter-unambp desiniter)))
  (let ((__function__ 'ldm-desiniter))
    (declare (ignorable __function__))
    (b* (((reterr)
          (c::expr-ident (c::ident "irrelevant")))
         ((desiniter desiniter) desiniter)
         ((when desiniter.designors)
          (reterr (msg "Unsupported designators ~x0."
                       desiniter.designors)))
         ((unless (initer-case desiniter.initer :single))
          (reterr (msg "Unsupported nested initializer ~x0."
                       desiniter.initer))))
      (ldm-expr (initer-single->expr desiniter.initer)))))

Theorem: exprp-of-ldm-desiniter.expr

(defthm exprp-of-ldm-desiniter.expr
  (b* (((mv acl2::?erp ?expr)
        (ldm-desiniter desiniter)))
    (c::exprp expr))
  :rule-classes :rewrite)

Theorem: ldm-desiniter-of-desiniter-fix-desiniter

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

Theorem: ldm-desiniter-desiniter-equiv-congruence-on-desiniter

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