arity

(in-package "ACL2")

(defsection std/system/arity
  :parents (std/system/function-queries)
  :short "Theorems about @(tsee arity)."
  (defthm arity-iff
    (iff (arity fn wrld)
      (or (consp fn) (function-symbolp fn wrld)))
    :hints (("Goal" :in-theory (enable arity)))))