		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)