		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-desiniter-list

Map a list of initializers with optional designations to a list of initializer expressions in the language definition.

Signature
(ldm-desiniter-list desiniters) → (mv erp exprs)
Arguments: desiniters — Guard (desiniter-listp desiniters).
Returns: exprs — Type (c::expr-listp exprs).

Definitions and Theorems

Function: ldm-desiniter-list

(defun ldm-desiniter-list (desiniters)
  (declare (xargs :guard (desiniter-listp desiniters)))
  (declare (xargs :guard (desiniter-list-unambp desiniters)))
  (let ((__function__ 'ldm-desiniter-list))
    (declare (ignorable __function__))
    (b* (((reterr) nil)
         ((when (endp desiniters)) (retok nil))
         ((erp expr1)
          (ldm-desiniter (car desiniters)))
         ((erp exprs1)
          (ldm-desiniter-list (cdr desiniters))))
      (retok (cons expr1 exprs1)))))

Theorem: expr-listp-of-ldm-desiniter-list.exprs

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

Theorem: ldm-desiniter-list-ok-when-desiniter-list-formalp

(defthm ldm-desiniter-list-ok-when-desiniter-list-formalp
  (implies (desiniter-list-formalp desiniters)
           (b* (((mv acl2::?erp ?exprs)
                 (ldm-desiniter-list desiniters)))
             (not erp))))

Theorem: ldm-desiniter-list-of-desiniter-list-fix-desiniters

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

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

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