		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-enumer-list

Map a list of enumerators to a list of identifiers in the language definition.

Signature
(ldm-enumer-list enumers) → (mv erp idents)
Arguments: enumers — Guard (enumer-listp enumers).
Returns: idents — Type (c::ident-listp idents).

Definitions and Theorems

Function: ldm-enumer-list

(defun ldm-enumer-list (enumers)
  (declare (xargs :guard (enumer-listp enumers)))
  (declare (xargs :guard (enumer-list-unambp enumers)))
  (let ((__function__ 'ldm-enumer-list))
    (declare (ignorable __function__))
    (b* (((reterr) nil)
         ((when (endp enumers)) (retok nil))
         ((erp ident) (ldm-enumer (car enumers)))
         ((erp idents)
          (ldm-enumer-list (cdr enumers))))
      (retok (cons ident idents)))))

Theorem: ident-listp-of-ldm-enumer-list.idents

(defthm ident-listp-of-ldm-enumer-list.idents
  (b* (((mv acl2::?erp ?idents)
        (ldm-enumer-list enumers)))
    (c::ident-listp idents))
  :rule-classes :rewrite)

Theorem: ldm-enumer-list-of-enumer-list-fix-enumers

(defthm ldm-enumer-list-of-enumer-list-fix-enumers
  (equal (ldm-enumer-list (enumer-list-fix enumers))
         (ldm-enumer-list enumers)))

Theorem: ldm-enumer-list-enumer-list-equiv-congruence-on-enumers

(defthm ldm-enumer-list-enumer-list-equiv-congruence-on-enumers
  (implies (enumer-list-equiv enumers enumers-equiv)
           (equal (ldm-enumer-list enumers)
                  (ldm-enumer-list enumers-equiv)))
  :rule-classes :congruence)