		Search-engine friendly clone of the ACL2 documentation.

Primitive-functions

Primitive-function-arity

Arith of a primitive function.

Signature
(primitive-function-arity name) → arity
Arguments: name — Guard (symbol-valuep name).
Returns: arity — Type (natp arity).

Definitions and Theorems

Function: primitive-function-arity

(defun primitive-function-arity (name)
 (declare (xargs :guard (symbol-valuep name)))
 (declare (xargs :guard (primitive-function-namep name)))
 (let ((__function__ 'primitive-function-arity))
  (declare (ignorable __function__))
  (cond
    ((symbol-value-equiv name (lift-symbol 'acl2-numberp))
     1)
    ((symbol-value-equiv name (lift-symbol 'rationalp))
     1)
    ((symbol-value-equiv name (lift-symbol 'integerp))
     1)
    ((symbol-value-equiv name (lift-symbol 'complex-rationalp))
     1)
    ((symbol-value-equiv name (lift-symbol 'complex))
     2)
    ((symbol-value-equiv name (lift-symbol 'realpart))
     1)
    ((symbol-value-equiv name (lift-symbol 'imagpart))
     1)
    ((symbol-value-equiv name (lift-symbol 'numerator))
     1)
    ((symbol-value-equiv name (lift-symbol 'denominator))
     1)
    ((symbol-value-equiv name (lift-symbol 'unary--))
     1)
    ((symbol-value-equiv name (lift-symbol 'unary-/))
     1)
    ((symbol-value-equiv name (lift-symbol 'binary-+))
     2)
    ((symbol-value-equiv name (lift-symbol 'binary-*))
     2)
    ((symbol-value-equiv name (lift-symbol '<))
     2)
    ((symbol-value-equiv name (lift-symbol 'characterp))
     1)
    ((symbol-value-equiv name (lift-symbol 'char-code))
     1)
    ((symbol-value-equiv name (lift-symbol 'code-char))
     1)
    ((symbol-value-equiv name (lift-symbol 'stringp))
     1)
    ((symbol-value-equiv name (lift-symbol 'coerce))
     2)
    ((symbol-value-equiv name (lift-symbol 'symbolp))
     1)
    ((symbol-value-equiv name (lift-symbol 'symbol-package-name))
     1)
    ((symbol-value-equiv name (lift-symbol 'symbol-name))
     1)
    ((symbol-value-equiv name
                         (lift-symbol 'intern-in-package-of-symbol))
     2)
    ((symbol-value-equiv name (lift-symbol 'consp))
     1)
    ((symbol-value-equiv name (lift-symbol 'cons))
     2)
    ((symbol-value-equiv name (lift-symbol 'car))
     1)
    ((symbol-value-equiv name (lift-symbol 'cdr))
     1)
    ((symbol-value-equiv name (lift-symbol 'pkg-imports))
     1)
    ((symbol-value-equiv name (lift-symbol 'pkg-witness))
     1)
    ((symbol-value-equiv name (lift-symbol 'equal))
     2)
    ((symbol-value-equiv name (lift-symbol 'if))
     3)
    ((symbol-value-equiv name (lift-symbol 'acl2::bad-atom<=))
     2)
    (t (prog2$ (impossible) 0)))))

Theorem: natp-of-primitive-function-arity

(defthm natp-of-primitive-function-arity
  (b* ((arity (primitive-function-arity name)))
    (natp arity))
  :rule-classes :rewrite)

Theorem: primitive-function-arity-of-symbol-value-fix-name

(defthm primitive-function-arity-of-symbol-value-fix-name
  (equal (primitive-function-arity (symbol-value-fix name))
         (primitive-function-arity name)))

Theorem: primitive-function-arity-symbol-value-equiv-congruence-on-name

(defthm
     primitive-function-arity-symbol-value-equiv-congruence-on-name
  (implies (symbol-value-equiv name name-equiv)
           (equal (primitive-function-arity name)
                  (primitive-function-arity name-equiv)))
  :rule-classes :congruence)