		Search-engine friendly clone of the ACL2 documentation.

Operations

Object-member-value?

Return the unique value associated to a member name in a JSON object, if the object has a member with that name.

Signature
(object-member-value? name object) → value?
Arguments: name — Guard (stringp name).; object — Guard (valuep object).
Returns: value? — Type (value-optionp value?).

While object-member-values is a general operation that never fails, in some cases a JSON object is expected to have no duplicate member names; indeed, the JSON standards recommend the absence of duplicate member names. In such cases, then, attempting to retrieve the value associated to a member name should result in at most one value. This operation can be used in these cases: it returns an optional value (i.e. a value or no value), but it conservatively checks that there are no other members with the same name; it does so by ensuring that the list returned by object-member-values contains at most one element. If there are duplicate member names, an error occurs.

Definitions and Theorems

Function: object-member-value?

(defun object-member-value? (name object)
 (declare (xargs :guard (and (stringp name) (valuep object))))
 (declare (xargs :guard (value-case object :object)))
 (let ((__function__ 'object-member-value?))
  (declare (ignorable __function__))
  (b* ((values (object-member-values name object)))
   (cond
    ((endp values) nil)
    ((= (len values) 1) (car values))
    (t
     (raise
      "The JSON object ~x0 ~
                     has multiple members with name ~x1."
      object name))))))

Theorem: value-optionp-of-object-member-value?

(defthm value-optionp-of-object-member-value?
  (b* ((value? (object-member-value? name object)))
    (value-optionp value?))
  :rule-classes :rewrite)