		Search-engine friendly clone of the ACL2 documentation.

Expressions

Vl-op-arity

Look up the arity of an operator.

Signature
(vl-op-arity x) → arity
Arguments: x — Guard (vl-op-p x).
Returns: arity — Type (maybe-natp arity).

(vl-op-arity x) determines the arity of the operator x by consulting the *vl-ops-table*. If x does not have a fixed arity (e.g., it might be a function call or concatenation operation), then we return nil.

We prefer to use vl-op-arity instead of looking up operators directly in the table, since this way we can disable vl-op-arity and avoid large case splits.

Definitions and Theorems

Function: vl-op-arity

(defun vl-op-arity (x)
  (declare (xargs :guard (vl-op-p x)))
  (let ((__function__ 'vl-op-arity))
    (declare (ignorable __function__))
    (b* ((op (vl-op-fix x))
         (info (cdr (assoc op (vl-ops-table)))))
      (vl-opinfo->arity info))))

Theorem: maybe-natp-of-vl-op-arity

(defthm maybe-natp-of-vl-op-arity
  (b* ((arity (vl-op-arity x)))
    (maybe-natp arity))
  :rule-classes :type-prescription)

Theorem: vl-op-arity-of-vl-op-fix-x

(defthm vl-op-arity-of-vl-op-fix-x
  (equal (vl-op-arity (vl-op-fix x))
         (vl-op-arity x)))

Theorem: vl-op-arity-vl-op-equiv-congruence-on-x

(defthm vl-op-arity-vl-op-equiv-congruence-on-x
  (implies (vl-op-equiv x x-equiv)
           (equal (vl-op-arity x)
                  (vl-op-arity x-equiv)))
  :rule-classes :congruence)

Subtopics

Arity-reasoning: Rules for reasoning about how many arguments an expression has.