		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax

Object-has-member-p

Check if a JSON object has some member with a given name.

Signature
(object-has-member-p name object) → yes/no
Arguments: name — Guard (stringp name).; object — Guard (valuep object).
Returns: yes/no — Type (booleanp yes/no).

The member may not be unique, i.e. if there are multiple members with the same name, this predicate returns t.

Definitions and Theorems

Function: object-has-member-p

(defun object-has-member-p (name object)
       (declare (xargs :guard (and (stringp name) (valuep object))))
       (declare (xargs :guard (value-case object :object)))
       (let ((__function__ 'object-has-member-p))
            (declare (ignorable __function__))
            (consp (object-member-values name object))))

Theorem: booleanp-of-object-has-member-p

(defthm booleanp-of-object-has-member-p
        (b* ((yes/no (object-has-member-p name object)))
            (booleanp yes/no))
        :rule-classes :rewrite)