(vl-parse-op-alist-p arity x) → *
Function:
(defun vl-parse-op-alist-p (arity x) (declare (xargs :guard t)) (let ((__function__ 'vl-parse-op-alist-p)) (declare (ignorable __function__)) (if (atom x) (not x) (and (consp (car x)) (vl-tokentype-p (caar x)) (or (and (eql arity 2) (vl-binaryop-p (cdar x))) (and (eql arity 1) (vl-unaryop-p (cdar x)))) (vl-parse-op-alist-p arity (cdr x))))))
Theorem:
(defthm vl-parse-op-alist-p-when-atom (implies (atom x) (equal (vl-parse-op-alist-p arity x) (not x))))
Theorem:
(defthm vl-parse-op-alist-p-when-consp (implies (consp x) (equal (vl-parse-op-alist-p arity x) (let ((a (car x)) (x (cdr x))) (and (consp a) (vl-tokentype-p (car a)) (or (and (eql arity 2) (vl-binaryop-p (cdr a))) (and (eql arity 1) (vl-unaryop-p (cdr a)))) (vl-parse-op-alist-p arity x))))))