Check if a JSON object has some member with a given name.
The member may not be unique,
i.e. if there are multiple members with the same name,
this predicate returns
(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))))
(defthm booleanp-of-object-has-member-p (b* ((yes/no (object-has-member-p name object))) (booleanp yes/no)) :rule-classes :rewrite)