		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax

Object-member-values-aux

Signature
(object-member-values-aux name members) → values
Arguments: name — Guard (stringp name).; members — Guard (member-listp members).
Returns: values — Type (value-listp values).

Definitions and Theorems

Function: object-member-values-aux

(defun object-member-values-aux (name members)
  (declare (xargs :guard (and (stringp name)
                              (member-listp members))))
  (let ((__function__ 'object-member-values-aux))
    (declare (ignorable __function__))
    (cond ((endp members) nil)
          ((equal name (member->name (car members)))
           (cons (member->value (car members))
                 (object-member-values-aux name (cdr members))))
          (t (object-member-values-aux name (cdr members))))))

Theorem: value-listp-of-object-member-values-aux

(defthm value-listp-of-object-member-values-aux
  (b* ((values (object-member-values-aux name members)))
    (value-listp values))
  :rule-classes :rewrite)