		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-ext-declon-list

Map a list of external declarations to the language definition.

Signature
(ldm-ext-declon-list extdecls) → (mv erp extdecls1)
Arguments: extdecls — Guard (ext-declon-listp extdecls).
Returns: extdecls1 — Type (c::ext-declon-listp extdecls1).

Definitions and Theorems

Function: ldm-ext-declon-list

(defun ldm-ext-declon-list (extdecls)
  (declare (xargs :guard (ext-declon-listp extdecls)))
  (declare (xargs :guard (ext-declon-list-unambp extdecls)))
  (let ((__function__ 'ldm-ext-declon-list))
    (declare (ignorable __function__))
    (b* (((reterr) nil)
         ((when (endp extdecls)) (retok nil))
         ((erp extdecl1)
          (ldm-ext-declon (car extdecls)))
         ((erp extdecls1)
          (ldm-ext-declon-list (cdr extdecls))))
      (retok (cons extdecl1 extdecls1)))))

Theorem: ext-declon-listp-of-ldm-ext-declon-list.extdecls1

(defthm ext-declon-listp-of-ldm-ext-declon-list.extdecls1
  (b* (((mv acl2::?erp ?extdecls1)
        (ldm-ext-declon-list extdecls)))
    (c::ext-declon-listp extdecls1))
  :rule-classes :rewrite)

Theorem: ldm-ext-declon-list-ok-when-ext-declon-list-formalp

(defthm ldm-ext-declon-list-ok-when-ext-declon-list-formalp
  (implies (ext-declon-list-formalp extdecls)
           (b* (((mv acl2::?erp ?extdecls1)
                 (ldm-ext-declon-list extdecls)))
             (not erp))))

Theorem: ldm-ext-declon-list-of-ext-declon-list-fix-extdecls

(defthm ldm-ext-declon-list-of-ext-declon-list-fix-extdecls
  (equal (ldm-ext-declon-list (ext-declon-list-fix extdecls))
         (ldm-ext-declon-list extdecls)))

Theorem: ldm-ext-declon-list-ext-declon-list-equiv-congruence-on-extdecls

(defthm
   ldm-ext-declon-list-ext-declon-list-equiv-congruence-on-extdecls
  (implies (ext-declon-list-equiv extdecls extdecls-equiv)
           (equal (ldm-ext-declon-list extdecls)
                  (ldm-ext-declon-list extdecls-equiv)))
  :rule-classes :congruence)