		Search-engine friendly clone of the ACL2 documentation.

Operations

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)