(vl-plural-p x) determines whether a description of a list should be plural instead of singluar.
(vl-plural-p x) → *
Output sometimes needs to be customized depending on whether a list contains only one element or many elements, e.g.,
(vl-plural-p x) is a stupid function to distinguish between the cases.
It returns true for a list like
We consider lists that have no elements to be plural. This gives the proper behavior in cases like:
(defun vl-plural-p$inline (x) (declare (xargs :guard t)) (let ((__function__ 'vl-plural-p)) (declare (ignorable __function__)) (mbe :logic (not (equal (len x) 1)) :exec (or (atom x) (not (atom (cdr x)))))))