		Search-engine friendly clone of the ACL2 documentation.

ACL2-built-ins

Arities-okp

check the arities of given function symbols

Example:
(arities-okp '((IF . 3) (CAR . 1) (CONS . 2)) (w state))

General Form:
(arities-okp alist w)

where alist is a symbol-alistp and w is an ACL2 logical world. The alist is presumed to pair :logic-mode function symbols with arities. The result is t or nil according to whether each symbol in the alist is a :logic-mode function symbol with the associated arity as its arity in w. See well-formedness-guarantee.

Function: arities-okp

(defun arities-okp (user-table w)
  (declare (xargs :guard (and (symbol-alistp user-table)
                              (plist-worldp-with-formals w))))
  (cond ((endp user-table) t)
        (t (and (equal (arity (car (car user-table)) w)
                       (cdr (car user-table)))
                (logicp (car (car user-table)) w)
                (arities-okp (cdr user-table) w)))))