		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Get-alternative-product

Find the type product of the alternative with a specified name.

Signature
(get-alternative-product name alts) → product
Arguments: name — Guard (identifierp name).; alts — Guard (alternative-listp alts).
Returns: product — Type (maybe-type-productp product).

We return the type product of the first alternative found with the specified name. Well-formed lists of alternatives have unique names, so the first one found is also the only one (if present at all).

Definitions and Theorems

Function: get-alternative-product

(defun get-alternative-product (name alts)
  (declare (xargs :guard (and (identifierp name)
                              (alternative-listp alts))))
  (let ((__function__ 'get-alternative-product))
    (declare (ignorable __function__))
    (b* (((when (endp alts)) nil)
         (alt (car alts))
         ((when (identifier-equiv name (alternative->name alt)))
          (alternative->product alt)))
      (get-alternative-product name (cdr alts)))))

Theorem: maybe-type-productp-of-get-alternative-product

(defthm maybe-type-productp-of-get-alternative-product
  (b* ((product (get-alternative-product name alts)))
    (maybe-type-productp product))
  :rule-classes :rewrite)

Theorem: get-alternative-product-of-identifier-fix-name

(defthm get-alternative-product-of-identifier-fix-name
  (equal (get-alternative-product (identifier-fix name)
                                  alts)
         (get-alternative-product name alts)))

Theorem: get-alternative-product-identifier-equiv-congruence-on-name

(defthm get-alternative-product-identifier-equiv-congruence-on-name
  (implies (identifier-equiv name name-equiv)
           (equal (get-alternative-product name alts)
                  (get-alternative-product name-equiv alts)))
  :rule-classes :congruence)

Theorem: get-alternative-product-of-alternative-list-fix-alts

(defthm get-alternative-product-of-alternative-list-fix-alts
  (equal (get-alternative-product name (alternative-list-fix alts))
         (get-alternative-product name alts)))

Theorem: get-alternative-product-alternative-list-equiv-congruence-on-alts

(defthm
  get-alternative-product-alternative-list-equiv-congruence-on-alts
  (implies (alternative-list-equiv alts alts-equiv)
           (equal (get-alternative-product name alts)
                  (get-alternative-product name alts-equiv)))
  :rule-classes :congruence)