(vl-arity-ok-p op args) → *
Function:
(defun vl-arity-ok-p (op args) (declare (xargs :guard (vl-op-p op))) (let ((__function__ 'vl-arity-ok-p)) (declare (ignorable __function__)) (let ((arity (vl-op-arity op))) (or (not arity) (equal (len args) arity)))))
Theorem:
(defthm vl-arity-ok-p-when-op-arity-known (implies (equal (vl-op-arity op) n) (equal (vl-arity-ok-p op args) (or (not n) (equal (len args) n)))))
Theorem:
(defthm vl-arity-ok-p-for-specific-operator (implies (syntaxp (quotep op)) (equal (vl-arity-ok-p op args) (let ((arity (vl-op-arity op))) (or (not arity) (equal (len args) arity))))))
Theorem:
(defthm vl-arity-ok-p-of-vl-op-fix-op (equal (vl-arity-ok-p (vl-op-fix op) args) (vl-arity-ok-p op args)))
Theorem:
(defthm vl-arity-ok-p-vl-op-equiv-congruence-on-op (implies (vl-op-equiv op op-equiv) (equal (vl-arity-ok-p op args) (vl-arity-ok-p op-equiv args))) :rule-classes :congruence)