		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-param-declon-list

Map a list of parameter declarations to a list of parameter declarations in the language definition.

Signature
(ldm-param-declon-list paramdecls) → (mv erp paramdecls1)
Arguments: paramdecls — Guard (param-declon-listp paramdecls).
Returns: paramdecls1 — Type (c::param-declon-listp paramdecls1).

Definitions and Theorems

Function: ldm-param-declon-list

(defun ldm-param-declon-list (paramdecls)
  (declare (xargs :guard (param-declon-listp paramdecls)))
  (declare (xargs :guard (param-declon-list-unambp paramdecls)))
  (let ((__function__ 'ldm-param-declon-list))
    (declare (ignorable __function__))
    (b* (((reterr) nil)
         ((when (endp paramdecls)) (retok nil))
         ((erp paramdecl1)
          (ldm-param-declon (car paramdecls)))
         ((erp paramdecls1)
          (ldm-param-declon-list (cdr paramdecls))))
      (retok (cons paramdecl1 paramdecls1)))))

Theorem: param-declon-listp-of-ldm-param-declon-list.paramdecls1

(defthm param-declon-listp-of-ldm-param-declon-list.paramdecls1
  (b* (((mv acl2::?erp ?paramdecls1)
        (ldm-param-declon-list paramdecls)))
    (c::param-declon-listp paramdecls1))
  :rule-classes :rewrite)

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

(defthm ldm-param-declon-list-ok-when-param-declon-list-formalp
  (implies (param-declon-list-formalp paramdecls)
           (b* (((mv acl2::?erp ?paramdecls1)
                 (ldm-param-declon-list paramdecls)))
             (not erp))))

Theorem: ldm-param-declon-list-of-param-declon-list-fix-paramdecls

(defthm ldm-param-declon-list-of-param-declon-list-fix-paramdecls
  (equal (ldm-param-declon-list (param-declon-list-fix paramdecls))
         (ldm-param-declon-list paramdecls)))

Theorem: ldm-param-declon-list-param-declon-list-equiv-congruence-on-paramdecls

(defthm
 ldm-param-declon-list-param-declon-list-equiv-congruence-on-paramdecls
 (implies (param-declon-list-equiv paramdecls paramdecls-equiv)
          (equal (ldm-param-declon-list paramdecls)
                 (ldm-param-declon-list paramdecls-equiv)))
 :rule-classes :congruence)