		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)